Theorem marypha1lem 8222

Description: Core induction for Philip Hall's marriage theorem. (Contributed by Stefan O'Rear, 19-Feb-2015.)

Assertion

Ref	Expression
marypha1lem	⊢ (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))

Distinct variable group:   𝐴,𝑏,𝑐,𝑑,𝑒

Proof of Theorem marypha1lem

Dummy variables 𝑎 𝑓 𝑔 ℎ 𝑖 𝑗 𝑘 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		xpeq1 5052	. . . . 5 ⊢ (𝑎 = 𝑓 → (𝑎 × 𝑏) = (𝑓 × 𝑏))
2	1	pweqd 4113	. . . 4 ⊢ (𝑎 = 𝑓 → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝑓 × 𝑏))
3		pweq 4111	. . . . . 6 ⊢ (𝑎 = 𝑓 → 𝒫 𝑎 = 𝒫 𝑓)
4	3	raleqdv 3121	. . . . 5 ⊢ (𝑎 = 𝑓 → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑)))
5		f1eq2 6010	. . . . . 6 ⊢ (𝑎 = 𝑓 → (𝑒:𝑎–1-1→V ↔ 𝑒:𝑓–1-1→V))
6	5	rexbidv 3034	. . . . 5 ⊢ (𝑎 = 𝑓 → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
7	4, 6	imbi12d 333	. . . 4 ⊢ (𝑎 = 𝑓 → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V)))
8	2, 7	raleqbidv 3129	. . 3 ⊢ (𝑎 = 𝑓 → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V)))
9	8	imbi2d 329	. 2 ⊢ (𝑎 = 𝑓 → ((𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
10		xpeq1 5052	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑎 × 𝑏) = (𝐴 × 𝑏))
11	10	pweqd 4113	. . . 4 ⊢ (𝑎 = 𝐴 → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝐴 × 𝑏))
12		pweq 4111	. . . . . 6 ⊢ (𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴)
13	12	raleqdv 3121	. . . . 5 ⊢ (𝑎 = 𝐴 → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑)))
14		f1eq2 6010	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑒:𝑎–1-1→V ↔ 𝑒:𝐴–1-1→V))
15	14	rexbidv 3034	. . . . 5 ⊢ (𝑎 = 𝐴 → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V))
16	13, 15	imbi12d 333	. . . 4 ⊢ (𝑎 = 𝐴 → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))
17	11, 16	raleqbidv 3129	. . 3 ⊢ (𝑎 = 𝐴 → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))
18	17	imbi2d 329	. 2 ⊢ (𝑎 = 𝐴 → ((𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V))))
19		bi2.04 375	. . . . 5 ⊢ ((𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ (𝑏 ∈ Fin → (𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
20	19	albii 1737	. . . 4 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ ∀𝑎(𝑏 ∈ Fin → (𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
21		19.21v 1855	. . . 4 ⊢ (∀𝑎(𝑏 ∈ Fin → (𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ (𝑏 ∈ Fin → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
22	20, 21	bitri 263	. . 3 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ (𝑏 ∈ Fin → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
23		0elpw 4760	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 𝒫 𝑔
24		f10 6081	. . . . . . . . . . . . 13 ⊢ ∅:∅–1-1→V
25		f1eq1 6009	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ∅ → (𝑒:∅–1-1→V ↔ ∅:∅–1-1→V))
26	25	rspcev 3282	. . . . . . . . . . . . 13 ⊢ ((∅ ∈ 𝒫 𝑔 ∧ ∅:∅–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V)
27	23, 24, 26	mp2an 704	. . . . . . . . . . . 12 ⊢ ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V
28		f1eq2 6010	. . . . . . . . . . . . 13 ⊢ (𝑓 = ∅ → (𝑒:𝑓–1-1→V ↔ 𝑒:∅–1-1→V))
29	28	rexbidv 3034	. . . . . . . . . . . 12 ⊢ (𝑓 = ∅ → (∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V))
30	27, 29	mpbiri 247	. . . . . . . . . . 11 ⊢ (𝑓 = ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
31	30	a1i 11	. . . . . . . . . 10 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑓 = ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
32		n0 3890	. . . . . . . . . . 11 ⊢ (𝑓 ≠ ∅ ↔ ∃𝑖 𝑖 ∈ 𝑓)
33		snelpwi 4839	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ 𝑓 → {𝑖} ∈ 𝒫 𝑓)
34		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑖} → 𝑑 = {𝑖})
35		imaeq2 5381	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑖} → (𝑔 “ 𝑑) = (𝑔 “ {𝑖}))
36	34, 35	breq12d 4596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = {𝑖} → (𝑑 ≼ (𝑔 “ 𝑑) ↔ {𝑖} ≼ (𝑔 “ {𝑖})))
37	36	rspcva 3280	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (({𝑖} ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → {𝑖} ≼ (𝑔 “ {𝑖}))
38		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑖 ∈ V
39	38	snnz 4252	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑖} ≠ ∅
40		snex 4835	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑖} ∈ V
41	40	0sdom 7976	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∅ ≺ {𝑖} ↔ {𝑖} ≠ ∅)
42	39, 41	mpbir 220	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∅ ≺ {𝑖}
43		sdomdomtr 7978	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∅ ≺ {𝑖} ∧ {𝑖} ≼ (𝑔 “ {𝑖})) → ∅ ≺ (𝑔 “ {𝑖}))
44	42, 43	mpan 702	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({𝑖} ≼ (𝑔 “ {𝑖}) → ∅ ≺ (𝑔 “ {𝑖}))
45		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑔 ∈ V
46	45	imaex 6996	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 “ {𝑖}) ∈ V
47	46	0sdom 7976	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∅ ≺ (𝑔 “ {𝑖}) ↔ (𝑔 “ {𝑖}) ≠ ∅)
48	44, 47	sylib 207	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑖} ≼ (𝑔 “ {𝑖}) → (𝑔 “ {𝑖}) ≠ ∅)
49	37, 48	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({𝑖} ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → (𝑔 “ {𝑖}) ≠ ∅)
50	49	expcom 450	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ({𝑖} ∈ 𝒫 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
51	33, 50	syl5 33	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → (𝑖 ∈ 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
52	51	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → (𝑖 ∈ 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
53	52	ad2antlr 759	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑖 ∈ 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
54	53	impr 647	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → (𝑔 “ {𝑖}) ≠ ∅)
55		n0 3890	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 “ {𝑖}) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}))
56	54, 55	sylib 207	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → ∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}))
57	45	imaex 6996	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 “ 𝑐) ∈ V
58	57	difexi 4736	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 “ 𝑐) ∖ {𝑗}) ∈ V
59	58	0dom 7975	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ∅ ≼ ((𝑔 “ 𝑐) ∖ {𝑗})
60		breq1 4586	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 = ∅ → (𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}) ↔ ∅ ≼ ((𝑔 “ 𝑐) ∖ {𝑗})))
61	59, 60	mpbiri 247	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = ∅ → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → (𝑐 = ∅ → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗})))
63		simpll 786	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)))
64		elpwi 4117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → 𝑐 ⊆ (𝑓 ∖ {𝑖}))
65	64	ad2antrl 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ⊆ (𝑓 ∖ {𝑖}))
66		difsnpss 4279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑖 ∈ 𝑓 ↔ (𝑓 ∖ {𝑖}) ⊊ 𝑓)
67	66	biimpi 205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑖 ∈ 𝑓 → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
68	67	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
69	65, 68	sspsstrd 3677	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ⊊ 𝑓)
70		simprr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≠ ∅)
71	69, 70	jca 553	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → (𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅))
72		psseq1 3656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → (ℎ ⊊ 𝑓 ↔ 𝑐 ⊊ 𝑓))
73		neeq1 2844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → (ℎ ≠ ∅ ↔ 𝑐 ≠ ∅))
74	72, 73	anbi12d 743	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (ℎ = 𝑐 → ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ↔ (𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅)))
75		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → ℎ = 𝑐)
76		imaeq2 5381	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → (𝑔 “ ℎ) = (𝑔 “ 𝑐))
77	75, 76	breq12d 4596	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (ℎ = 𝑐 → (ℎ ≺ (𝑔 “ ℎ) ↔ 𝑐 ≺ (𝑔 “ 𝑐)))
78	74, 77	imbi12d 333	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (ℎ = 𝑐 → (((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ↔ ((𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅) → 𝑐 ≺ (𝑔 “ 𝑐))))
79	78	spv 2248	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) → ((𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅) → 𝑐 ≺ (𝑔 “ 𝑐)))
80	63, 71, 79	sylc 63	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≺ (𝑔 “ 𝑐))
81		domdifsn 7928	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 ≺ (𝑔 “ 𝑐) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
82	80, 81	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
83	82	expr 641	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → (𝑐 ≠ ∅ → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗})))
84	62, 83	pm2.61dne 2868	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
85	84	adantlrr 753	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
86	85	adantll 746	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
87		df-ss 3554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 ⊆ (𝑓 ∖ {𝑖}) ↔ (𝑐 ∩ (𝑓 ∖ {𝑖})) = 𝑐)
88	64, 87	sylib 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → (𝑐 ∩ (𝑓 ∖ {𝑖})) = 𝑐)
89	88	imaeq2d 5385	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → (𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) = (𝑔 “ 𝑐))
90	89	ineq1d 3775	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})))
91	90	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})))
92		indif2 3829	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ {𝑗})
93		imassrn 5396	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 “ 𝑐) ⊆ ran 𝑔
94		elpwi 4117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → 𝑔 ⊆ (𝑓 × 𝑏))
95		rnss 5275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → ran 𝑔 ⊆ ran (𝑓 × 𝑏))
96		rnxpss 5485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ran (𝑓 × 𝑏) ⊆ 𝑏
97	95, 96	syl6ss 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → ran 𝑔 ⊆ 𝑏)
98	94, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ran 𝑔 ⊆ 𝑏)
99	93, 98	syl5ss 3579	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔 “ 𝑐) ⊆ 𝑏)
100		df-ss 3554	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 “ 𝑐) ⊆ 𝑏 ↔ ((𝑔 “ 𝑐) ∩ 𝑏) = (𝑔 “ 𝑐))
101	99, 100	sylib 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ((𝑔 “ 𝑐) ∩ 𝑏) = (𝑔 “ 𝑐))
102	101	difeq1d 3689	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ {𝑗}) = ((𝑔 “ 𝑐) ∖ {𝑗}))
103	102	ad2antrl 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ {𝑗}) = ((𝑔 “ 𝑐) ∖ {𝑗}))
104	92, 103	syl5eq 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∖ {𝑗}))
105	104	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∖ {𝑗}))
106	91, 105	eqtrd 2644	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∖ {𝑗}))
107	86, 106	breqtrrd 4611	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})))
108	107	ralrimiva 2949	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})))
109		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑑 → 𝑐 = 𝑑)
110		imainrect 5494	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑐) = ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗}))
111		imaeq2 5381	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = 𝑑 → ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑐) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
112	110, 111	syl5eqr 2658	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑑 → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
113	109, 112	breq12d 4596	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑑 → (𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
114	113	cbvralv 3147	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
115	108, 114	sylib 207	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
116	115	adantllr 751	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
117		inss2 3796	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))
118		difss 3699	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 ∖ {𝑗}) ⊆ 𝑏
119		xpss2 5152	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∖ {𝑗}) ⊆ 𝑏 → ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏))
120	118, 119	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏)
121	117, 120	sstri 3577	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏)
122	45	inex1 4727	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ V
123	122	elpw 4114	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏) ↔ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏))
124	121, 123	mpbir 220	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)
125		simpllr 795	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)))
126	67	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
127	126	ad2antll 761	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
128		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑓 ∈ V
129	128	difexi 4736	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 ∖ {𝑖}) ∈ V
130		psseq1 3656	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (𝑎 ⊊ 𝑓 ↔ (𝑓 ∖ {𝑖}) ⊊ 𝑓))
131		xpeq1 5052	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (𝑎 × 𝑏) = ((𝑓 ∖ {𝑖}) × 𝑏))
132	131	pweqd 4113	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → 𝒫 (𝑎 × 𝑏) = 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏))
133		pweq 4111	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → 𝒫 𝑎 = 𝒫 (𝑓 ∖ {𝑖}))
134	133	raleqdv 3121	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑)))
135		f1eq2 6010	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (𝑒:𝑎–1-1→V ↔ 𝑒:(𝑓 ∖ {𝑖})–1-1→V))
136	135	rexbidv 3034	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))
137	134, 136	imbi12d 333	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
138	132, 137	raleqbidv 3129	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
139	130, 138	imbi12d 333	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → ((𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ ((𝑓 ∖ {𝑖}) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))))
140	129, 139	spcv 3272	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → ((𝑓 ∖ {𝑖}) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
141	125, 127, 140	sylc 63	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))
142		imaeq1 5380	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (𝑐 “ 𝑑) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
143	142	breq2d 4595	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (𝑑 ≼ (𝑐 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
144	143	ralbidv 2969	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
145		pweq 4111	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝒫 𝑐 = 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))))
146	145	rexeqdv 3122	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
147	144, 146	imbi12d 333	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ((∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
148	147	rspcva 3280	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
149	124, 141, 148	sylancr 694	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
150	116, 149	mpd 15	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V)
151		f1eq1 6009	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑘 → (𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ 𝑘:(𝑓 ∖ {𝑖})–1-1→V))
152	151	cbvrexv 3148	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ ∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V)
153	150, 152	sylib 207	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V)
154		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑗 ∈ V
155	38, 154	elimasn 5409	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑗 ∈ (𝑔 “ {𝑖}) ↔ ⟨𝑖, 𝑗⟩ ∈ 𝑔)
156	155	biimpi 205	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 ∈ (𝑔 “ {𝑖}) → ⟨𝑖, 𝑗⟩ ∈ 𝑔)
157	156	snssd 4281	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑗 ∈ (𝑔 “ {𝑖}) → {⟨𝑖, 𝑗⟩} ⊆ 𝑔)
158	157	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → {⟨𝑖, 𝑗⟩} ⊆ 𝑔)
159		elpwi 4117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))))
160		inss1 3795	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ 𝑔
161	159, 160	syl6ss 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ 𝑔)
162	161	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → 𝑘 ⊆ 𝑔)
163	158, 162	unssd 3751	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ⊆ 𝑔)
164	45	elpw2 4755	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔 ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ⊆ 𝑔)
165	163, 164	sylibr 223	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔)
166	165	ad2ant2lr 780	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔)
167	38, 154	f1osn 6088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ {⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗}
168	167	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → {⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗})
169		f1f1orn 6061	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘:(𝑓 ∖ {𝑖})–1-1→V → 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘)
170	169	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘)
171		disjdif 3992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅)
173		incom 3767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ({𝑗} ∩ ran 𝑘) = (ran 𝑘 ∩ {𝑗})
174	159, 117	syl6ss 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))
175		rnss 5275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) → ran 𝑘 ⊆ ran ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))
176		rnxpss 5485	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ran ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ (𝑏 ∖ {𝑗})
177	175, 176	syl6ss 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) → ran 𝑘 ⊆ (𝑏 ∖ {𝑗}))
178	174, 177	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ran 𝑘 ⊆ (𝑏 ∖ {𝑗}))
179		incom 3767	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ({𝑗} ∩ (𝑏 ∖ {𝑗}))
180		disjdif 3992	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ({𝑗} ∩ (𝑏 ∖ {𝑗})) = ∅
181	179, 180	eqtri 2632	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ∅
182		ssdisj 3978	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((ran 𝑘 ⊆ (𝑏 ∖ {𝑗}) ∧ ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ∅) → (ran 𝑘 ∩ {𝑗}) = ∅)
183	178, 181, 182	sylancl 693	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (ran 𝑘 ∩ {𝑗}) = ∅)
184	173, 183	syl5eq 2656	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ({𝑗} ∩ ran 𝑘) = ∅)
185	184	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({𝑗} ∩ ran 𝑘) = ∅)
186		f1oun 6069	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((({⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗} ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘) ∧ (({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅ ∧ ({𝑗} ∩ ran 𝑘) = ∅)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
187	168, 170, 172, 185, 186	syl22anc 1319	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
188	187	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
189		snssi 4280	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 ∈ 𝑓 → {𝑖} ⊆ 𝑓)
190	189	ad2antrl 760	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → {𝑖} ⊆ 𝑓)
191		undif 4001	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ({𝑖} ⊆ 𝑓 ↔ ({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓)
192	190, 191	sylib 207	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → ({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓)
193		f1oeq2 6041	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓 → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘)))
194	192, 193	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘)))
195	194	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘)))
196	188, 195	mpbid 221	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘))
197		f1of1 6049	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→({𝑗} ∪ ran 𝑘))
198		ssv 3588	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ({𝑗} ∪ ran 𝑘) ⊆ V
199		f1ss 6019	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→({𝑗} ∪ ran 𝑘) ∧ ({𝑗} ∪ ran 𝑘) ⊆ V) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V)
200	197, 198, 199	sylancl 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V)
201	196, 200	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V)
202		f1eq1 6009	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑒 = ({⟨𝑖, 𝑗⟩} ∪ 𝑘) → (𝑒:𝑓–1-1→V ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V))
203	202	rspcev 3282	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔 ∧ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
204	166, 201, 203	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
205	204	rexlimdvaa 3014	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
206	205	ex 449	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
207	206	adantr 480	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
208	207	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
209	208	impr 647	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
210	209	adantllr 751	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
211	153, 210	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
212	211	expr 641	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
213	212	expd 451	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑖 ∈ 𝑓 → (𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
214	213	impr 647	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → (𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
215	214	exlimdv 1848	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → (∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
216	56, 215	mpd 15	. . . . . . . . . . . . 13 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
217	216	expr 641	. . . . . . . . . . . 12 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑖 ∈ 𝑓 → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
218	217	exlimdv 1848	. . . . . . . . . . 11 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (∃𝑖 𝑖 ∈ 𝑓 → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
219	32, 218	syl5bi 231	. . . . . . . . . 10 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑓 ≠ ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
220	31, 219	pm2.61dne 2868	. . . . . . . . 9 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
221		exanali 1773	. . . . . . . . . 10 ⊢ (∃ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) ↔ ¬ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)))
222		simprll 798	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ℎ ⊊ 𝑓)
223		pssss 3664	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ ⊊ 𝑓 → ℎ ⊆ 𝑓)
224	222, 223	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ℎ ⊆ 𝑓)
225		sspwb 4844	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ ⊆ 𝑓 ↔ 𝒫 ℎ ⊆ 𝒫 𝑓)
226	224, 225	sylib 207	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → 𝒫 ℎ ⊆ 𝒫 𝑓)
227		simplrr 797	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))
228		ssralv 3629	. . . . . . . . . . . . . . . . . 18 ⊢ (𝒫 ℎ ⊆ 𝒫 𝑓 → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑔 “ 𝑑)))
229	226, 227, 228	sylc 63	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑔 “ 𝑑))
230		elpwi 4117	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ∈ 𝒫 ℎ → 𝑑 ⊆ ℎ)
231		resima2 5352	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ⊆ ℎ → ((𝑔 ↾ ℎ) “ 𝑑) = (𝑔 “ 𝑑))
232	230, 231	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ 𝒫 ℎ → ((𝑔 ↾ ℎ) “ 𝑑) = (𝑔 “ 𝑑))
233	232	eqcomd 2616	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ 𝒫 ℎ → (𝑔 “ 𝑑) = ((𝑔 ↾ ℎ) “ 𝑑))
234	233	breq2d 4595	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ 𝒫 ℎ → (𝑑 ≼ (𝑔 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑)))
235	234	ralbiia 2962	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑔 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑))
236	229, 235	sylib 207	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑))
237		simplrl 796	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → 𝑔 ∈ 𝒫 (𝑓 × 𝑏))
238		ssres 5344	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ⊆ ((𝑓 × 𝑏) ↾ ℎ))
239		df-res 5050	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 × 𝑏) ↾ ℎ) = ((𝑓 × 𝑏) ∩ (ℎ × V))
240		inxp 5176	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 × 𝑏) ∩ (ℎ × V)) = ((𝑓 ∩ ℎ) × (𝑏 ∩ V))
241		inss2 3796	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 ∩ ℎ) ⊆ ℎ
242		inss1 3795	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∩ V) ⊆ 𝑏
243		xpss12 5148	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑓 ∩ ℎ) ⊆ ℎ ∧ (𝑏 ∩ V) ⊆ 𝑏) → ((𝑓 ∩ ℎ) × (𝑏 ∩ V)) ⊆ (ℎ × 𝑏))
244	241, 242, 243	mp2an 704	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 ∩ ℎ) × (𝑏 ∩ V)) ⊆ (ℎ × 𝑏)
245	240, 244	eqsstri 3598	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 × 𝑏) ∩ (ℎ × V)) ⊆ (ℎ × 𝑏)
246	239, 245	eqsstri 3598	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 × 𝑏) ↾ ℎ) ⊆ (ℎ × 𝑏)
247	238, 246	syl6ss 3580	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ⊆ (ℎ × 𝑏))
248	94, 247	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ⊆ (ℎ × 𝑏))
249	45	resex 5363	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ↾ ℎ) ∈ V
250	249	elpw 4114	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ↾ ℎ) ∈ 𝒫 (ℎ × 𝑏) ↔ (𝑔 ↾ ℎ) ⊆ (ℎ × 𝑏))
251	248, 250	sylibr 223	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ∈ 𝒫 (ℎ × 𝑏))
252	237, 251	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (𝑔 ↾ ℎ) ∈ 𝒫 (ℎ × 𝑏))
253		simpllr 795	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)))
254		psseq1 3656	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ℎ → (𝑎 ⊊ 𝑓 ↔ ℎ ⊊ 𝑓))
255		xpeq1 5052	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = ℎ → (𝑎 × 𝑏) = (ℎ × 𝑏))
256	255	pweqd 4113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = ℎ → 𝒫 (𝑎 × 𝑏) = 𝒫 (ℎ × 𝑏))
257		pweq 4111	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = ℎ → 𝒫 𝑎 = 𝒫 ℎ)
258	257	raleqdv 3121	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = ℎ → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑)))
259		f1eq2 6010	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = ℎ → (𝑒:𝑎–1-1→V ↔ 𝑒:ℎ–1-1→V))
260	259	rexbidv 3034	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = ℎ → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V))
261	258, 260	imbi12d 333	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = ℎ → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V)))
262	256, 261	raleqbidv 3129	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ℎ → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V)))
263	254, 262	imbi12d 333	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ℎ → ((𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ (ℎ ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V))))
264	263	spv 2248	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → (ℎ ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V)))
265	253, 222, 264	sylc 63	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V))
266		imaeq1 5380	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (𝑐 “ 𝑑) = ((𝑔 ↾ ℎ) “ 𝑑))
267	266	breq2d 4595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (𝑑 ≼ (𝑐 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑)))
268	267	ralbidv 2969	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑)))
269		pweq 4111	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑔 ↾ ℎ) → 𝒫 𝑐 = 𝒫 (𝑔 ↾ ℎ))
270	269	rexeqdv 3122	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V))
271	268, 270	imbi12d 333	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑔 ↾ ℎ) → ((∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V) ↔ (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V)))
272	271	rspcva 3280	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔 ↾ ℎ) ∈ 𝒫 (ℎ × 𝑏) ∧ ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V)) → (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V))
273	252, 265, 272	syl2anc 691	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V))
274	236, 273	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V)
275		f1eq1 6009	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑖 → (𝑒:ℎ–1-1→V ↔ 𝑖:ℎ–1-1→V))
276	275	cbvrexv 3148	. . . . . . . . . . . . . . 15 ⊢ (∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V ↔ ∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V)
277	274, 276	sylib 207	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V)
278	223	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) → ℎ ⊆ 𝑓)
279	278	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ⊆ 𝑓)
280		elpwi 4117	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → 𝑐 ⊆ (𝑓 ∖ ℎ))
281		difss 3699	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 ∖ ℎ) ⊆ 𝑓
282	280, 281	syl6ss 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → 𝑐 ⊆ 𝑓)
283	282	adantl 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ⊆ 𝑓)
284	279, 283	unssd 3751	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ⊆ 𝑓)
285	128	elpw2 4755	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ ∪ 𝑐) ∈ 𝒫 𝑓 ↔ (ℎ ∪ 𝑐) ⊆ 𝑓)
286	284, 285	sylibr 223	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ∈ 𝒫 𝑓)
287		simprr 792	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))
288	287	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))
289		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = (ℎ ∪ 𝑐) → 𝑑 = (ℎ ∪ 𝑐))
290		imaeq2 5381	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = (ℎ ∪ 𝑐) → (𝑔 “ 𝑑) = (𝑔 “ (ℎ ∪ 𝑐)))
291	289, 290	breq12d 4596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (ℎ ∪ 𝑐) → (𝑑 ≼ (𝑔 “ 𝑑) ↔ (ℎ ∪ 𝑐) ≼ (𝑔 “ (ℎ ∪ 𝑐))))
292	291	rspcva 3280	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((ℎ ∪ 𝑐) ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → (ℎ ∪ 𝑐) ≼ (𝑔 “ (ℎ ∪ 𝑐)))
293	286, 288, 292	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ≼ (𝑔 “ (ℎ ∪ 𝑐)))
294		imaundi 5464	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 “ (ℎ ∪ 𝑐)) = ((𝑔 “ ℎ) ∪ (𝑔 “ 𝑐))
295		undif2 3996	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ((𝑔 “ ℎ) ∪ (𝑔 “ 𝑐))
296	294, 295	eqtr4i 2635	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 “ (ℎ ∪ 𝑐)) = ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
297	293, 296	syl6breq 4624	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ≼ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))))
298		simp-4l 802	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑓 ∈ Fin)
299	298, 279	ssfid 8068	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ∈ Fin)
300		vex 3176	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℎ ∈ V
301	300	elpw 4114	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ ∈ 𝒫 𝑓 ↔ ℎ ⊆ 𝑓)
302	279, 301	sylibr 223	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ∈ 𝒫 𝑓)
303		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑑 = ℎ → 𝑑 = ℎ)
304		imaeq2 5381	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑑 = ℎ → (𝑔 “ 𝑑) = (𝑔 “ ℎ))
305	303, 304	breq12d 4596	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 = ℎ → (𝑑 ≼ (𝑔 “ 𝑑) ↔ ℎ ≼ (𝑔 “ ℎ)))
306	305	rspcva 3280	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((ℎ ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → ℎ ≼ (𝑔 “ ℎ))
307	302, 288, 306	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ≼ (𝑔 “ ℎ))
308		simplrr 797	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ¬ ℎ ≺ (𝑔 “ ℎ))
309		bren2 7872	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ ≈ (𝑔 “ ℎ) ↔ (ℎ ≼ (𝑔 “ ℎ) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)))
310	307, 308, 309	sylanbrc 695	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ≈ (𝑔 “ ℎ))
311	310	ensymd 7893	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (𝑔 “ ℎ) ≈ ℎ)
312		incom 3767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∩ 𝑐) = (𝑐 ∩ ℎ)
313		ssdifin0 4002	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 ⊆ (𝑓 ∖ ℎ) → (𝑐 ∩ ℎ) = ∅)
314	312, 313	syl5eq 2656	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 ⊆ (𝑓 ∖ ℎ) → (ℎ ∩ 𝑐) = ∅)
315	280, 314	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → (ℎ ∩ 𝑐) = ∅)
316	315	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∩ 𝑐) = ∅)
317		disjdif 3992	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 “ ℎ) ∩ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ∅
318	317	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ((𝑔 “ ℎ) ∩ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ∅)
319		domunfican 8118	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ ∈ Fin ∧ (𝑔 “ ℎ) ≈ ℎ) ∧ ((ℎ ∩ 𝑐) = ∅ ∧ ((𝑔 “ ℎ) ∩ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ∅)) → ((ℎ ∪ 𝑐) ≼ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) ↔ 𝑐 ≼ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))))
320	299, 311, 316, 318, 319	syl22anc 1319	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ((ℎ ∪ 𝑐) ≼ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) ↔ 𝑐 ≼ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))))
321	297, 320	mpbid 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
322	101	difeq1d 3689	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)) = ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
323	322	ad2antrl 760	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)) = ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
324	323	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)) = ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
325	321, 324	breqtrrd 4611	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ≼ (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)))
326		df-ss 3554	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 ⊆ (𝑓 ∖ ℎ) ↔ (𝑐 ∩ (𝑓 ∖ ℎ)) = 𝑐)
327	280, 326	sylib 207	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → (𝑐 ∩ (𝑓 ∖ ℎ)) = 𝑐)
328	327	imaeq2d 5385	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → (𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) = (𝑔 “ 𝑐))
329	328	ineq1d 3775	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = ((𝑔 “ 𝑐) ∩ (𝑏 ∖ (𝑔 “ ℎ))))
330		indif2 3829	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 “ 𝑐) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ))
331	329, 330	syl6eq 2660	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)))
332	331	adantl 481	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)))
333	325, 332	breqtrrd 4611	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))))
334	333	ralrimiva 2949	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))))
335		imainrect 5494	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑐) = ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ)))
336		imaeq2 5381	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑑 → ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑐) = ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
337	335, 336	syl5eqr 2658	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = 𝑑 → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
338	109, 337	breq12d 4596	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑑 → (𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑)))
339	338	cbvralv 3147	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
340	334, 339	sylib 207	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
341	340	adantllr 751	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
342		inss2 3796	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))
343		difss 3699	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∖ (𝑔 “ ℎ)) ⊆ 𝑏
344		xpss2 5152	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∖ (𝑔 “ ℎ)) ⊆ 𝑏 → ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) ⊆ ((𝑓 ∖ ℎ) × 𝑏))
345	343, 344	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) ⊆ ((𝑓 ∖ ℎ) × 𝑏)
346	342, 345	sstri 3577	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ ((𝑓 ∖ ℎ) × 𝑏)
347	45	inex1 4727	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ V
348	347	elpw 4114	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏) ↔ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ ((𝑓 ∖ ℎ) × 𝑏))
349	346, 348	mpbir 220	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)
350		incom 3767	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∩ ℎ) = (ℎ ∩ 𝑓)
351		df-ss 3554	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ⊆ 𝑓 ↔ (ℎ ∩ 𝑓) = ℎ)
352	223, 351	sylib 207	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ⊊ 𝑓 → (ℎ ∩ 𝑓) = ℎ)
353	350, 352	syl5eq 2656	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ ⊊ 𝑓 → (𝑓 ∩ ℎ) = ℎ)
354	353	neeq1d 2841	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ ⊊ 𝑓 → ((𝑓 ∩ ℎ) ≠ ∅ ↔ ℎ ≠ ∅))
355	354	biimpar 501	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → (𝑓 ∩ ℎ) ≠ ∅)
356		disj4 3977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 ∩ ℎ) = ∅ ↔ ¬ (𝑓 ∖ ℎ) ⊊ 𝑓)
357	356	bicomi 213	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝑓 ∖ ℎ) ⊊ 𝑓 ↔ (𝑓 ∩ ℎ) = ∅)
358	357	necon1abii 2830	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∩ ℎ) ≠ ∅ ↔ (𝑓 ∖ ℎ) ⊊ 𝑓)
359	355, 358	sylib 207	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → (𝑓 ∖ ℎ) ⊊ 𝑓)
360	359	ad2antrl 760	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (𝑓 ∖ ℎ) ⊊ 𝑓)
361	128	difexi 4736	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∖ ℎ) ∈ V
362		psseq1 3656	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (𝑎 ⊊ 𝑓 ↔ (𝑓 ∖ ℎ) ⊊ 𝑓))
363		xpeq1 5052	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (𝑎 × 𝑏) = ((𝑓 ∖ ℎ) × 𝑏))
364	363	pweqd 4113	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (𝑓 ∖ ℎ) → 𝒫 (𝑎 × 𝑏) = 𝒫 ((𝑓 ∖ ℎ) × 𝑏))
365		pweq 4111	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (𝑓 ∖ ℎ) → 𝒫 𝑎 = 𝒫 (𝑓 ∖ ℎ))
366	365	raleqdv 3121	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑)))
367		f1eq2 6010	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (𝑒:𝑎–1-1→V ↔ 𝑒:(𝑓 ∖ ℎ)–1-1→V))
368	367	rexbidv 3034	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V))
369	366, 368	imbi12d 333	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (𝑓 ∖ ℎ) → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)))
370	364, 369	raleqbidv 3129	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)))
371	362, 370	imbi12d 333	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑓 ∖ ℎ) → ((𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ ((𝑓 ∖ ℎ) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V))))
372	361, 371	spcv 3272	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → ((𝑓 ∖ ℎ) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)))
373	253, 360, 372	sylc 63	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V))
374		imaeq1 5380	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (𝑐 “ 𝑑) = ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
375	374	breq2d 4595	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (𝑑 ≼ (𝑐 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑)))
376	375	ralbidv 2969	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑)))
377		pweq 4111	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝒫 𝑐 = 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))))
378	377	rexeqdv 3122	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V))
379	376, 378	imbi12d 333	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → ((∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V)))
380	379	rspcva 3280	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V))
381	349, 373, 380	sylancr 694	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V))
382	341, 381	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V)
383		f1eq1 6009	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑗 → (𝑒:(𝑓 ∖ ℎ)–1-1→V ↔ 𝑗:(𝑓 ∖ ℎ)–1-1→V))
384	383	cbvrexv 3148	. . . . . . . . . . . . . . 15 ⊢ (∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V ↔ ∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V)
385	382, 384	sylib 207	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V)
386		elpwi 4117	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → 𝑖 ⊆ (𝑔 ↾ ℎ))
387		resss 5342	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ↾ ℎ) ⊆ 𝑔
388	386, 387	syl6ss 3580	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → 𝑖 ⊆ 𝑔)
389	388	adantr 480	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V) → 𝑖 ⊆ 𝑔)
390	389	ad2antlr 759	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑖 ⊆ 𝑔)
391		elpwi 4117	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝑗 ⊆ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))))
392		inss1 3795	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ 𝑔
393	391, 392	syl6ss 3580	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝑗 ⊆ 𝑔)
394	393	ad2antrl 760	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑗 ⊆ 𝑔)
395	390, 394	unssd 3751	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗) ⊆ 𝑔)
396	45	elpw2 4755	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∪ 𝑗) ∈ 𝒫 𝑔 ↔ (𝑖 ∪ 𝑗) ⊆ 𝑔)
397	395, 396	sylibr 223	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗) ∈ 𝒫 𝑔)
398		f1f1orn 6061	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖:ℎ–1-1→V → 𝑖:ℎ–1-1-onto→ran 𝑖)
399	398	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V) → 𝑖:ℎ–1-1-onto→ran 𝑖)
400	399	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑖:ℎ–1-1-onto→ran 𝑖)
401		f1f1orn 6061	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗:(𝑓 ∖ ℎ)–1-1→V → 𝑗:(𝑓 ∖ ℎ)–1-1-onto→ran 𝑗)
402	401	ad2antll 761	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑗:(𝑓 ∖ ℎ)–1-1-onto→ran 𝑗)
403		disjdif 3992	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ∩ (𝑓 ∖ ℎ)) = ∅
404	403	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ℎ ∩ (𝑓 ∖ ℎ)) = ∅)
405		rnss 5275	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ⊆ (𝑔 ↾ ℎ) → ran 𝑖 ⊆ ran (𝑔 ↾ ℎ))
406	386, 405	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → ran 𝑖 ⊆ ran (𝑔 ↾ ℎ))
407		df-ima 5051	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔 “ ℎ) = ran (𝑔 ↾ ℎ)
408	406, 407	syl6sseqr 3615	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → ran 𝑖 ⊆ (𝑔 “ ℎ))
409	408	adantr 480	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V) → ran 𝑖 ⊆ (𝑔 “ ℎ))
410	409	ad2antlr 759	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ran 𝑖 ⊆ (𝑔 “ ℎ))
411		incom 3767	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 “ ℎ) ∩ ran 𝑗) = (ran 𝑗 ∩ (𝑔 “ ℎ))
412	391, 342	syl6ss 3580	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝑗 ⊆ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))
413		rnss 5275	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ⊆ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) → ran 𝑗 ⊆ ran ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))
414	412, 413	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → ran 𝑗 ⊆ ran ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))
415		rnxpss 5485	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ran ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) ⊆ (𝑏 ∖ (𝑔 “ ℎ))
416	414, 415	syl6ss 3580	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → ran 𝑗 ⊆ (𝑏 ∖ (𝑔 “ ℎ)))
417	416	ad2antrl 760	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ran 𝑗 ⊆ (𝑏 ∖ (𝑔 “ ℎ)))
418		incom 3767	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏 ∖ (𝑔 “ ℎ)) ∩ (𝑔 “ ℎ)) = ((𝑔 “ ℎ) ∩ (𝑏 ∖ (𝑔 “ ℎ)))
419		disjdif 3992	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔 “ ℎ) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = ∅
420	418, 419	eqtri 2632	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∖ (𝑔 “ ℎ)) ∩ (𝑔 “ ℎ)) = ∅
421		ssdisj 3978	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ran 𝑗 ⊆ (𝑏 ∖ (𝑔 “ ℎ)) ∧ ((𝑏 ∖ (𝑔 “ ℎ)) ∩ (𝑔 “ ℎ)) = ∅) → (ran 𝑗 ∩ (𝑔 “ ℎ)) = ∅)
422	417, 420, 421	sylancl 693	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ran 𝑗 ∩ (𝑔 “ ℎ)) = ∅)
423	411, 422	syl5eq 2656	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ((𝑔 “ ℎ) ∩ ran 𝑗) = ∅)
424		ssdisj 3978	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ran 𝑖 ⊆ (𝑔 “ ℎ) ∧ ((𝑔 “ ℎ) ∩ ran 𝑗) = ∅) → (ran 𝑖 ∩ ran 𝑗) = ∅)
425	410, 423, 424	syl2anc 691	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ran 𝑖 ∩ ran 𝑗) = ∅)
426		f1oun 6069	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑖:ℎ–1-1-onto→ran 𝑖 ∧ 𝑗:(𝑓 ∖ ℎ)–1-1-onto→ran 𝑗) ∧ ((ℎ ∩ (𝑓 ∖ ℎ)) = ∅ ∧ (ran 𝑖 ∩ ran 𝑗) = ∅)) → (𝑖 ∪ 𝑗):(ℎ ∪ (𝑓 ∖ ℎ))–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
427	400, 402, 404, 425, 426	syl22anc 1319	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):(ℎ ∪ (𝑓 ∖ ℎ))–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
428		undif 4001	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ ⊆ 𝑓 ↔ (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
429	428	biimpi 205	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ⊆ 𝑓 → (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
430	429	adantl 481	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) → (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
431	430	ad2antrr 758	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
432		f1oeq2 6041	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓 → ((𝑖 ∪ 𝑗):(ℎ ∪ (𝑓 ∖ ℎ))–1-1-onto→(ran 𝑖 ∪ ran 𝑗) ↔ (𝑖 ∪ 𝑗):𝑓–1-1-onto→(ran 𝑖 ∪ ran 𝑗)))
433	431, 432	syl 17	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ((𝑖 ∪ 𝑗):(ℎ ∪ (𝑓 ∖ ℎ))–1-1-onto→(ran 𝑖 ∪ ran 𝑗) ↔ (𝑖 ∪ 𝑗):𝑓–1-1-onto→(ran 𝑖 ∪ ran 𝑗)))
434	427, 433	mpbid 221	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):𝑓–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
435		f1of1 6049	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∪ 𝑗):𝑓–1-1-onto→(ran 𝑖 ∪ ran 𝑗) → (𝑖 ∪ 𝑗):𝑓–1-1→(ran 𝑖 ∪ ran 𝑗))
436	434, 435	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):𝑓–1-1→(ran 𝑖 ∪ ran 𝑗))
437		ssv 3588	. . . . . . . . . . . . . . . . . . 19 ⊢ (ran 𝑖 ∪ ran 𝑗) ⊆ V
438		f1ss 6019	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∪ 𝑗):𝑓–1-1→(ran 𝑖 ∪ ran 𝑗) ∧ (ran 𝑖 ∪ ran 𝑗) ⊆ V) → (𝑖 ∪ 𝑗):𝑓–1-1→V)
439	436, 437, 438	sylancl 693	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):𝑓–1-1→V)
440		f1eq1 6009	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖 ∪ 𝑗) → (𝑒:𝑓–1-1→V ↔ (𝑖 ∪ 𝑗):𝑓–1-1→V))
441	440	rspcev 3282	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∪ 𝑗) ∈ 𝒫 𝑔 ∧ (𝑖 ∪ 𝑗):𝑓–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
442	397, 439, 441	syl2anc 691	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
443	442	rexlimdvaa 3014	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
444	443	rexlimdvaa 3014	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) → (∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
445	237, 224, 444	syl2anc 691	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
446	277, 385, 445	mp2d 47	. . . . . . . . . . . . 13 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
447	446	ex 449	. . . . . . . . . . . 12 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
448	447	exlimdv 1848	. . . . . . . . . . 11 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (∃ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
449	448	imp 444	. . . . . . . . . 10 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∃ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
450	221, 449	sylan2br 492	. . . . . . . . 9 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ¬ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
451	220, 450	pm2.61dan 828	. . . . . . . 8 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
452	451	exp32 629	. . . . . . 7 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
453	452	ralrimiv 2948	. . . . . 6 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → ∀𝑔 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
454		imaeq1 5380	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → (𝑔 “ 𝑑) = (𝑐 “ 𝑑))
455	454	breq2d 4595	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → (𝑑 ≼ (𝑔 “ 𝑑) ↔ 𝑑 ≼ (𝑐 “ 𝑑)))
456	455	ralbidv 2969	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑)))
457		pweq 4111	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → 𝒫 𝑔 = 𝒫 𝑐)
458	457	rexeqdv 3122	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
459	456, 458	imbi12d 333	. . . . . . 7 ⊢ (𝑔 = 𝑐 → ((∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V)))
460	459	cbvralv 3147	. . . . . 6 ⊢ (∀𝑔 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
461	453, 460	sylib 207	. . . . 5 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
462	461	exp31 628	. . . 4 ⊢ (𝑓 ∈ Fin → (𝑏 ∈ Fin → (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
463	462	a2d 29	. . 3 ⊢ (𝑓 ∈ Fin → ((𝑏 ∈ Fin → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
464	22, 463	syl5bi 231	. 2 ⊢ (𝑓 ∈ Fin → (∀𝑎(𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
465	9, 18, 464	findcard3 8088	1 ⊢ (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 195   ∧ wa 383  ∀wal 1473   = wceq 1475  ∃wex 1695   ∈ wcel 1977   ≠ wne 2780  ∀wral 2896  ∃wrex 2897  Vcvv 3173   ∖ cdif 3537   ∪ cun 3538   ∩ cin 3539   ⊆ wss 3540   ⊊ wpss 3541  ∅c0 3874  𝒫 cpw 4108  {csn 4125  ⟨cop 4131   class class class wbr 4583   × cxp 5036  ran crn 5039   ↾ cres 5040   “ cima 5041  –1-1→wf1 5801  –1-1-onto→wf1o 5803   ≈ cen 7838   ≼ cdom 7839   ≺ csdm 7840  Fincfn 7841

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-rab 2905  df-v 3175  df-sbc 3403  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-br 4584  df-opab 4644  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-om 6958  df-1o 7447  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845

This theorem is referenced by:  marypha1  8223