Theorem marypha1lem 9425

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 5665	. . . . 5 ⊢ (𝑎 = 𝑓 → (𝑎 × 𝑏) = (𝑓 × 𝑏))
2	1	pweqd 4574	. . . 4 ⊢ (𝑎 = 𝑓 → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝑓 × 𝑏))
3		pweq 4571	. . . . . 6 ⊢ (𝑎 = 𝑓 → 𝒫 𝑎 = 𝒫 𝑓)
4	3	raleqdv 3320	. . . . 5 ⊢ (𝑎 = 𝑓 → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑)))
5		f1eq2 6774	. . . . . 6 ⊢ (𝑎 = 𝑓 → (𝑒:𝑎–1-1→V ↔ 𝑒:𝑓–1-1→V))
6	5	rexbidv 3187	. . . . 5 ⊢ (𝑎 = 𝑓 → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
7	4, 6	imbi12d 347	. . . 4 ⊢ (𝑎 = 𝑓 → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V)))
8	2, 7	raleqbidv 3335	. . 3 ⊢ (𝑎 = 𝑓 → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V)))
9	8	imbi2d 343	. 2 ⊢ (𝑎 = 𝑓 → ((𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
10		xpeq1 5665	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑎 × 𝑏) = (𝐴 × 𝑏))
11	10	pweqd 4574	. . . 4 ⊢ (𝑎 = 𝐴 → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝐴 × 𝑏))
12		pweq 4571	. . . . . 6 ⊢ (𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴)
13	12	raleqdv 3320	. . . . 5 ⊢ (𝑎 = 𝐴 → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑)))
14		f1eq2 6774	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑒:𝑎–1-1→V ↔ 𝑒:𝐴–1-1→V))
15	14	rexbidv 3187	. . . . 5 ⊢ (𝑎 = 𝐴 → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V))
16	13, 15	imbi12d 347	. . . 4 ⊢ (𝑎 = 𝐴 → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))
17	11, 16	raleqbidv 3335	. . 3 ⊢ (𝑎 = 𝐴 → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))
18	17	imbi2d 343	. 2 ⊢ (𝑎 = 𝐴 → ((𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V))))
19		bi2.04 392	. . . . 5 ⊢ ((𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ (𝑏 ∈ Fin → (𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
20	19	albii 1852	. . . 4 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ ∀𝑎(𝑏 ∈ Fin → (𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
21		19.21v 1972	. . . 4 ⊢ (∀𝑎(𝑏 ∈ Fin → (𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ (𝑏 ∈ Fin → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
22	20, 21	bitri 278	. . 3 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ (𝑏 ∈ Fin → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
23		0elpw 5317	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 𝒫 𝑔
24		f10 6858	. . . . . . . . . . . . 13 ⊢ ∅:∅–1-1→V
25		f1eq1 6773	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ∅ → (𝑒:∅–1-1→V ↔ ∅:∅–1-1→V))
26	25	rspcev 3577	. . . . . . . . . . . . 13 ⊢ ((∅ ∈ 𝒫 𝑔 ∧ ∅:∅–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V)
27	23, 24, 26	mp2an 705	. . . . . . . . . . . 12 ⊢ ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V
28		f1eq2 6774	. . . . . . . . . . . . 13 ⊢ (𝑓 = ∅ → (𝑒:𝑓–1-1→V ↔ 𝑒:∅–1-1→V))
29	28	rexbidv 3187	. . . . . . . . . . . 12 ⊢ (𝑓 = ∅ → (∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V))
30	27, 29	mpbiri 261	. . . . . . . . . . 11 ⊢ (𝑓 = ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
31	30	a1i 11	. . . . . . . . . 10 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑓 = ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
32		n0 4300	. . . . . . . . . . 11 ⊢ (𝑓 ≠ ∅ ↔ ∃𝑖 𝑖 ∈ 𝑓)
33		snelpwi 5412	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ 𝑓 → {𝑖} ∈ 𝒫 𝑓)
34		id 23	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑖} → 𝑑 = {𝑖})
35		imaeq2 6048	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑖} → (𝑔 “ 𝑑) = (𝑔 “ {𝑖}))
36	34, 35	breq12d 5116	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = {𝑖} → (𝑑 ≼ (𝑔 “ 𝑑) ↔ {𝑖} ≼ (𝑔 “ {𝑖})))
37	36	rspcva 3575	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (({𝑖} ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → {𝑖} ≼ (𝑔 “ {𝑖}))
38		vex 3455	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑖 ∈ V
39	38	snnz 4737	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑖} ≠ ∅
40		vsnex 5393	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑖} ∈ V
41	40	0sdom 9127	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∅ ≺ {𝑖} ↔ {𝑖} ≠ ∅)
42	39, 41	mpbir 234	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∅ ≺ {𝑖}
43		sdomdomtr 9129	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∅ ≺ {𝑖} ∧ {𝑖} ≼ (𝑔 “ {𝑖})) → ∅ ≺ (𝑔 “ {𝑖}))
44	42, 43	mpan 703	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({𝑖} ≼ (𝑔 “ {𝑖}) → ∅ ≺ (𝑔 “ {𝑖}))
45		vex 3455	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑔 ∈ V
46	45	imaex 7926	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 “ {𝑖}) ∈ V
47	46	0sdom 9127	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∅ ≺ (𝑔 “ {𝑖}) ↔ (𝑔 “ {𝑖}) ≠ ∅)
48	44, 47	sylib 221	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑖} ≼ (𝑔 “ {𝑖}) → (𝑔 “ {𝑖}) ≠ ∅)
49	37, 48	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({𝑖} ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → (𝑔 “ {𝑖}) ≠ ∅)
50	49	expcom 419	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ({𝑖} ∈ 𝒫 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
51	33, 50	syl5 35	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → (𝑖 ∈ 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
52	51	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → (𝑖 ∈ 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
53	52	ad2antlr 740	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑖 ∈ 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
54	53	impr 460	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → (𝑔 “ {𝑖}) ≠ ∅)
55		n0 4300	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 “ {𝑖}) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}))
56	54, 55	sylib 221	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → ∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}))
57	45	imaex 7926	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 “ 𝑐) ∈ V
58	57	difexi 5292	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 “ 𝑐) ∖ {𝑗}) ∈ V
59	58	0dom 9126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ∅ ≼ ((𝑔 “ 𝑐) ∖ {𝑗})
60		breq1 5106	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 = ∅ → (𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}) ↔ ∅ ≼ ((𝑔 “ 𝑐) ∖ {𝑗})))
61	59, 60	mpbiri 261	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = ∅ → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → (𝑐 = ∅ → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗})))
63		simpll 779	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)))
64		elpwi 4564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → 𝑐 ⊆ (𝑓 ∖ {𝑖}))
65	64	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ⊆ (𝑓 ∖ {𝑖}))
66		difsnpss 4770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑖 ∈ 𝑓 ↔ (𝑓 ∖ {𝑖}) ⊊ 𝑓)
67	66	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑖 ∈ 𝑓 → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
68	67	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
69	65, 68	sspsstrd 4060	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ⊊ 𝑓)
70		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≠ ∅)
71	69, 70	jca 521	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → (𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅))
72		psseq1 4038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → (ℎ ⊊ 𝑓 ↔ 𝑐 ⊊ 𝑓))
73		neeq1 3018	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → (ℎ ≠ ∅ ↔ 𝑐 ≠ ∅))
74	72, 73	anbi12d 644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (ℎ = 𝑐 → ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ↔ (𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅)))
75		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → ℎ = 𝑐)
76		imaeq2 6048	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → (𝑔 “ ℎ) = (𝑔 “ 𝑐))
77	75, 76	breq12d 5116	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (ℎ = 𝑐 → (ℎ ≺ (𝑔 “ ℎ) ↔ 𝑐 ≺ (𝑔 “ 𝑐)))
78	74, 77	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (ℎ = 𝑐 → (((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ↔ ((𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅) → 𝑐 ≺ (𝑔 “ 𝑐))))
79	78	spvv 2021	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) → ((𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅) → 𝑐 ≺ (𝑔 “ 𝑐)))
80	63, 71, 79	sylc 66	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≺ (𝑔 “ 𝑐))
81		domdifsn 9079	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 ≺ (𝑔 “ 𝑐) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
82	80, 81	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
83	82	expr 462	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → (𝑐 ≠ ∅ → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗})))
84	62, 83	pm2.61dne 3042	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
85	84	adantlrr 734	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
86	85	adantll 727	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
87		dfss2 3917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 ⊆ (𝑓 ∖ {𝑖}) ↔ (𝑐 ∩ (𝑓 ∖ {𝑖})) = 𝑐)
88	64, 87	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → (𝑐 ∩ (𝑓 ∖ {𝑖})) = 𝑐)
89	88	imaeq2d 6052	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → (𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) = (𝑔 “ 𝑐))
90	89	ineq1d 4165	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})))
91	90	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})))
92		indif2 4227	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ {𝑗})
93		imassrn 6197	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 “ 𝑐) ⊆ ran 𝑔
94		elpwi 4564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → 𝑔 ⊆ (𝑓 × 𝑏))
95		rnss 5921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → ran 𝑔 ⊆ ran (𝑓 × 𝑏))
96		rnxpss 6164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ran (𝑓 × 𝑏) ⊆ 𝑏
97	95, 96	sstrdi 3943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → ran 𝑔 ⊆ 𝑏)
98	94, 97	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ran 𝑔 ⊆ 𝑏)
99	93, 98	sstrid 3942	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔 “ 𝑐) ⊆ 𝑏)
100		dfss2 3917	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 “ 𝑐) ⊆ 𝑏 ↔ ((𝑔 “ 𝑐) ∩ 𝑏) = (𝑔 “ 𝑐))
101	99, 100	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ((𝑔 “ 𝑐) ∩ 𝑏) = (𝑔 “ 𝑐))
102	101	difeq1d 4073	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ {𝑗}) = ((𝑔 “ 𝑐) ∖ {𝑗}))
103	102	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ {𝑗}) = ((𝑔 “ 𝑐) ∖ {𝑗}))
104	92, 103	eqtrid 2808	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∖ {𝑗}))
105	104	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∖ {𝑗}))
106	91, 105	eqtrd 2796	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∖ {𝑗}))
107	86, 106	breqtrrd 5133	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})))
108	107	ralrimiva 3155	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})))
109		id 23	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑑 → 𝑐 = 𝑑)
110		imainrect 6173	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑐) = ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗}))
111		imaeq2 6048	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = 𝑑 → ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑐) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
112	110, 111	eqtr3id 2810	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑑 → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
113	109, 112	breq12d 5116	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑑 → (𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
114	113	cbvralvw 3241	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
115	108, 114	sylib 221	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
116	115	adantllr 732	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
117		inss2 4183	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))
118		difss 4083	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 ∖ {𝑗}) ⊆ 𝑏
119		xpss2 5671	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∖ {𝑗}) ⊆ 𝑏 → ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏))
120	118, 119	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏)
121	117, 120	sstri 3940	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏)
122	45	inex1 5277	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ V
123	122	elpw 4561	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏) ↔ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏))
124	121, 123	mpbir 234	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)
125		simpllr 788	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)))
126	67	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
127	126	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
128		vex 3455	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑓 ∈ V
129	128	difexi 5292	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 ∖ {𝑖}) ∈ V
130		psseq1 4038	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (𝑎 ⊊ 𝑓 ↔ (𝑓 ∖ {𝑖}) ⊊ 𝑓))
131		xpeq1 5665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (𝑎 × 𝑏) = ((𝑓 ∖ {𝑖}) × 𝑏))
132	131	pweqd 4574	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → 𝒫 (𝑎 × 𝑏) = 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏))
133		pweq 4571	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → 𝒫 𝑎 = 𝒫 (𝑓 ∖ {𝑖}))
134	133	raleqdv 3320	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑)))
135		f1eq2 6774	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (𝑒:𝑎–1-1→V ↔ 𝑒:(𝑓 ∖ {𝑖})–1-1→V))
136	135	rexbidv 3187	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))
137	134, 136	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
138	132, 137	raleqbidv 3335	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
139	130, 138	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → ((𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ ((𝑓 ∖ {𝑖}) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))))
140	129, 139	spcv 3560	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → ((𝑓 ∖ {𝑖}) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
141	125, 127, 140	sylc 66	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))
142		imaeq1 6047	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (𝑐 “ 𝑑) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
143	142	breq2d 5115	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (𝑑 ≼ (𝑐 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
144	143	ralbidv 3186	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
145		pweq 4571	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝒫 𝑐 = 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))))
146	145	rexeqdv 3321	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
147	144, 146	imbi12d 347	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ((∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
148	147	rspcva 3575	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
149	124, 141, 148	sylancr 599	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
150	116, 149	mpd 16	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V)
151		f1eq1 6773	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑘 → (𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ 𝑘:(𝑓 ∖ {𝑖})–1-1→V))
152	151	cbvrexvw 3242	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ ∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V)
153	150, 152	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V)
154		vex 3455	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑗 ∈ V
155	38, 154	elimasn 6088	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑗 ∈ (𝑔 “ {𝑖}) ↔ ⟨𝑖, 𝑗⟩ ∈ 𝑔)
156	155	biimpi 219	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 ∈ (𝑔 “ {𝑖}) → ⟨𝑖, 𝑗⟩ ∈ 𝑔)
157	156	snssd 4747	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑗 ∈ (𝑔 “ {𝑖}) → {⟨𝑖, 𝑗⟩} ⊆ 𝑔)
158	157	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → {⟨𝑖, 𝑗⟩} ⊆ 𝑔)
159		elpwi 4564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))))
160		inss1 4182	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ 𝑔
161	159, 160	sstrdi 3943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ 𝑔)
162	161	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → 𝑘 ⊆ 𝑔)
163	158, 162	unssd 4138	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ⊆ 𝑔)
164	45	elpw2 5296	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔 ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ⊆ 𝑔)
165	163, 164	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔)
166	165	ad2ant2lr 761	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔)
167	38, 154	f1osn 6866	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ {⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗}
168	167	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → {⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗})
169		f1f1orn 6836	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘:(𝑓 ∖ {𝑖})–1-1→V → 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘)
170	169	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘)
171		disjdif 4426	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅)
173		incom 4155	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ({𝑗} ∩ ran 𝑘) = (ran 𝑘 ∩ {𝑗})
174	159, 117	sstrdi 3943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))
175		rnss 5921	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) → ran 𝑘 ⊆ ran ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))
176		rnxpss 6164	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ran ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ (𝑏 ∖ {𝑗})
177	175, 176	sstrdi 3943	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) → ran 𝑘 ⊆ (𝑏 ∖ {𝑗}))
178	174, 177	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ran 𝑘 ⊆ (𝑏 ∖ {𝑗}))
179		disjdifr 4427	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ∅
180		ssdisj 4413	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((ran 𝑘 ⊆ (𝑏 ∖ {𝑗}) ∧ ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ∅) → (ran 𝑘 ∩ {𝑗}) = ∅)
181	178, 179, 180	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (ran 𝑘 ∩ {𝑗}) = ∅)
182	173, 181	eqtrid 2808	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ({𝑗} ∩ ran 𝑘) = ∅)
183	182	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({𝑗} ∩ ran 𝑘) = ∅)
184		f1oun 6844	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((({⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗} ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘) ∧ (({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅ ∧ ({𝑗} ∩ ran 𝑘) = ∅)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
185	168, 170, 172, 183, 184	syl22anc 852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
186	185	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
187		snssi 4746	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 ∈ 𝑓 → {𝑖} ⊆ 𝑓)
188	187	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → {𝑖} ⊆ 𝑓)
189		undif 4438	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ({𝑖} ⊆ 𝑓 ↔ ({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓)
190	188, 189	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → ({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓)
191	190	f1oeq2d 6820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘)))
192	191	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘)))
193	186, 192	mpbid 235	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘))
194		f1of1 6823	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→({𝑗} ∪ ran 𝑘))
195		ssv 3955	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ({𝑗} ∪ ran 𝑘) ⊆ V
196		f1ss 6785	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→({𝑗} ∪ ran 𝑘) ∧ ({𝑗} ∪ ran 𝑘) ⊆ V) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V)
197	194, 195, 196	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V)
198	193, 197	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V)
199		f1eq1 6773	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑒 = ({⟨𝑖, 𝑗⟩} ∪ 𝑘) → (𝑒:𝑓–1-1→V ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V))
200	199	rspcev 3577	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔 ∧ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
201	166, 198, 200	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
202	201	rexlimdvaa 3165	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
203	202	ex 418	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
204	203	adantr 486	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
205	204	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
206	205	impr 460	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
207	206	adantllr 732	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
208	153, 207	mpd 16	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
209	208	expr 462	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
210	209	expd 421	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑖 ∈ 𝑓 → (𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
211	210	impr 460	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → (𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
212	211	exlimdv 1966	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → (∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
213	56, 212	mpd 16	. . . . . . . . . . . . 13 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
214	213	expr 462	. . . . . . . . . . . 12 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑖 ∈ 𝑓 → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
215	214	exlimdv 1966	. . . . . . . . . . 11 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (∃𝑖 𝑖 ∈ 𝑓 → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
216	32, 215	biimtrid 245	. . . . . . . . . 10 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑓 ≠ ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
217	31, 216	pm2.61dne 3042	. . . . . . . . 9 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
218		exanali 1892	. . . . . . . . . 10 ⊢ (∃ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) ↔ ¬ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)))
219		simprll 791	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ℎ ⊊ 𝑓)
220		pssss 4046	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ ⊊ 𝑓 → ℎ ⊆ 𝑓)
221	219, 220	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ℎ ⊆ 𝑓)
222	221	sspwd 4570	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → 𝒫 ℎ ⊆ 𝒫 𝑓)
223		simplrr 790	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))
224		ssralv 4000	. . . . . . . . . . . . . . . . . 18 ⊢ (𝒫 ℎ ⊆ 𝒫 𝑓 → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑔 “ 𝑑)))
225	222, 223, 224	sylc 66	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑔 “ 𝑑))
226		elpwi 4564	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ∈ 𝒫 ℎ → 𝑑 ⊆ ℎ)
227		resima2 6057	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ⊆ ℎ → ((𝑔 ↾ ℎ) “ 𝑑) = (𝑔 “ 𝑑))
228	226, 227	syl 18	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ 𝒫 ℎ → ((𝑔 ↾ ℎ) “ 𝑑) = (𝑔 “ 𝑑))
229	228	eqcomd 2767	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ 𝒫 ℎ → (𝑔 “ 𝑑) = ((𝑔 ↾ ℎ) “ 𝑑))
230	229	breq2d 5115	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ 𝒫 ℎ → (𝑑 ≼ (𝑔 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑)))
231	230	ralbiia 3107	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑔 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑))
232	225, 231	sylib 221	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑))
233		imaeq1 6047	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (𝑐 “ 𝑑) = ((𝑔 ↾ ℎ) “ 𝑑))
234	233	breq2d 5115	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (𝑑 ≼ (𝑐 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑)))
235	234	ralbidv 3186	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑)))
236		pweq 4571	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ↾ ℎ) → 𝒫 𝑐 = 𝒫 (𝑔 ↾ ℎ))
237	236	rexeqdv 3321	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V))
238	235, 237	imbi12d 347	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑔 ↾ ℎ) → ((∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V) ↔ (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V)))
239		simpllr 788	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)))
240		psseq1 4038	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ℎ → (𝑎 ⊊ 𝑓 ↔ ℎ ⊊ 𝑓))
241		xpeq1 5665	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = ℎ → (𝑎 × 𝑏) = (ℎ × 𝑏))
242	241	pweqd 4574	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = ℎ → 𝒫 (𝑎 × 𝑏) = 𝒫 (ℎ × 𝑏))
243		pweq 4571	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = ℎ → 𝒫 𝑎 = 𝒫 ℎ)
244	243	raleqdv 3320	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = ℎ → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑)))
245		f1eq2 6774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = ℎ → (𝑒:𝑎–1-1→V ↔ 𝑒:ℎ–1-1→V))
246	245	rexbidv 3187	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = ℎ → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V))
247	244, 246	imbi12d 347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = ℎ → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V)))
248	242, 247	raleqbidv 3335	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ℎ → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V)))
249	240, 248	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ℎ → ((𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ (ℎ ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V))))
250	249	spvv 2021	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → (ℎ ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V)))
251	239, 219, 250	sylc 66	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V))
252		simplrl 789	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → 𝑔 ∈ 𝒫 (𝑓 × 𝑏))
253		ssres 5994	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ⊆ ((𝑓 × 𝑏) ↾ ℎ))
254		df-res 5663	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 × 𝑏) ↾ ℎ) = ((𝑓 × 𝑏) ∩ (ℎ × V))
255		inxp 5809	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 × 𝑏) ∩ (ℎ × V)) = ((𝑓 ∩ ℎ) × (𝑏 ∩ V))
256		inss2 4183	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 ∩ ℎ) ⊆ ℎ
257		inss1 4182	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∩ V) ⊆ 𝑏
258		xpss12 5666	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑓 ∩ ℎ) ⊆ ℎ ∧ (𝑏 ∩ V) ⊆ 𝑏) → ((𝑓 ∩ ℎ) × (𝑏 ∩ V)) ⊆ (ℎ × 𝑏))
259	256, 257, 258	mp2an 705	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 ∩ ℎ) × (𝑏 ∩ V)) ⊆ (ℎ × 𝑏)
260	255, 259	eqsstri 3977	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 × 𝑏) ∩ (ℎ × V)) ⊆ (ℎ × 𝑏)
261	254, 260	eqsstri 3977	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 × 𝑏) ↾ ℎ) ⊆ (ℎ × 𝑏)
262	253, 261	sstrdi 3943	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ⊆ (ℎ × 𝑏))
263	94, 262	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ⊆ (ℎ × 𝑏))
264	45	resex 6018	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ↾ ℎ) ∈ V
265	264	elpw 4561	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ↾ ℎ) ∈ 𝒫 (ℎ × 𝑏) ↔ (𝑔 ↾ ℎ) ⊆ (ℎ × 𝑏))
266	263, 265	sylibr 237	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ∈ 𝒫 (ℎ × 𝑏))
267	252, 266	syl 18	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (𝑔 ↾ ℎ) ∈ 𝒫 (ℎ × 𝑏))
268	238, 251, 267	rspcdva 3578	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V))
269	232, 268	mpd 16	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V)
270		f1eq1 6773	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑖 → (𝑒:ℎ–1-1→V ↔ 𝑖:ℎ–1-1→V))
271	270	cbvrexvw 3242	. . . . . . . . . . . . . . 15 ⊢ (∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V ↔ ∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V)
272	269, 271	sylib 221	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V)
273		id 23	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (ℎ ∪ 𝑐) → 𝑑 = (ℎ ∪ 𝑐))
274		imaeq2 6048	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (ℎ ∪ 𝑐) → (𝑔 “ 𝑑) = (𝑔 “ (ℎ ∪ 𝑐)))
275	273, 274	breq12d 5116	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = (ℎ ∪ 𝑐) → (𝑑 ≼ (𝑔 “ 𝑑) ↔ (ℎ ∪ 𝑐) ≼ (𝑔 “ (ℎ ∪ 𝑐))))
276		simprr 785	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))
277	276	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))
278	220	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) → ℎ ⊆ 𝑓)
279	278	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ⊆ 𝑓)
280		elpwi 4564	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → 𝑐 ⊆ (𝑓 ∖ ℎ))
281		difss 4083	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 ∖ ℎ) ⊆ 𝑓
282	280, 281	sstrdi 3943	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → 𝑐 ⊆ 𝑓)
283	282	adantl 487	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ⊆ 𝑓)
284	279, 283	unssd 4138	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ⊆ 𝑓)
285	128	elpw2 5296	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ ∪ 𝑐) ∈ 𝒫 𝑓 ↔ (ℎ ∪ 𝑐) ⊆ 𝑓)
286	284, 285	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ∈ 𝒫 𝑓)
287	275, 277, 286	rspcdva 3578	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ≼ (𝑔 “ (ℎ ∪ 𝑐)))
288		imaundi 6141	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 “ (ℎ ∪ 𝑐)) = ((𝑔 “ ℎ) ∪ (𝑔 “ 𝑐))
289		undif2 4431	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ((𝑔 “ ℎ) ∪ (𝑔 “ 𝑐))
290	288, 289	eqtr4i 2787	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 “ (ℎ ∪ 𝑐)) = ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
291	287, 290	breqtrdi 5146	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ≼ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))))
292		simp-4l 795	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑓 ∈ Fin)
293	292, 279	ssfid 9260	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ∈ Fin)
294		id 23	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 = ℎ → 𝑑 = ℎ)
295		imaeq2 6048	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 = ℎ → (𝑔 “ 𝑑) = (𝑔 “ ℎ))
296	294, 295	breq12d 5116	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = ℎ → (𝑑 ≼ (𝑔 “ 𝑑) ↔ ℎ ≼ (𝑔 “ ℎ)))
297		vex 3455	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℎ ∈ V
298	297	elpw 4561	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ ∈ 𝒫 𝑓 ↔ ℎ ⊆ 𝑓)
299	279, 298	sylibr 237	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ∈ 𝒫 𝑓)
300	296, 277, 299	rspcdva 3578	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ≼ (𝑔 “ ℎ))
301		simplrr 790	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ¬ ℎ ≺ (𝑔 “ ℎ))
302		bren2 9010	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ ≈ (𝑔 “ ℎ) ↔ (ℎ ≼ (𝑔 “ ℎ) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)))
303	300, 301, 302	sylanbrc 595	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ≈ (𝑔 “ ℎ))
304	303	ensymd 9032	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (𝑔 “ ℎ) ≈ ℎ)
305		incom 4155	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∩ 𝑐) = (𝑐 ∩ ℎ)
306		ssdifin0 4441	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 ⊆ (𝑓 ∖ ℎ) → (𝑐 ∩ ℎ) = ∅)
307	305, 306	eqtrid 2808	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 ⊆ (𝑓 ∖ ℎ) → (ℎ ∩ 𝑐) = ∅)
308	280, 307	syl 18	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → (ℎ ∩ 𝑐) = ∅)
309	308	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∩ 𝑐) = ∅)
310		disjdif 4426	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 “ ℎ) ∩ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ∅
311	310	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ((𝑔 “ ℎ) ∩ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ∅)
312		domunfican 9313	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ ∈ Fin ∧ (𝑔 “ ℎ) ≈ ℎ) ∧ ((ℎ ∩ 𝑐) = ∅ ∧ ((𝑔 “ ℎ) ∩ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ∅)) → ((ℎ ∪ 𝑐) ≼ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) ↔ 𝑐 ≼ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))))
313	293, 304, 309, 311, 312	syl22anc 852	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ((ℎ ∪ 𝑐) ≼ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) ↔ 𝑐 ≼ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))))
314	291, 313	mpbid 235	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
315	101	difeq1d 4073	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)) = ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
316	315	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)) = ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
317	316	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)) = ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
318	314, 317	breqtrrd 5133	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ≼ (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)))
319		dfss2 3917	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 ⊆ (𝑓 ∖ ℎ) ↔ (𝑐 ∩ (𝑓 ∖ ℎ)) = 𝑐)
320	280, 319	sylib 221	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → (𝑐 ∩ (𝑓 ∖ ℎ)) = 𝑐)
321	320	imaeq2d 6052	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → (𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) = (𝑔 “ 𝑐))
322	321	ineq1d 4165	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = ((𝑔 “ 𝑐) ∩ (𝑏 ∖ (𝑔 “ ℎ))))
323		indif2 4227	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 “ 𝑐) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ))
324	322, 323	eqtrdi 2812	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)))
325	324	adantl 487	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)))
326	318, 325	breqtrrd 5133	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))))
327	326	ralrimiva 3155	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))))
328		imainrect 6173	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑐) = ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ)))
329		imaeq2 6048	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑑 → ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑐) = ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
330	328, 329	eqtr3id 2810	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = 𝑑 → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
331	109, 330	breq12d 5116	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑑 → (𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑)))
332	331	cbvralvw 3241	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
333	327, 332	sylib 221	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
334	333	adantllr 732	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
335		inss2 4183	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))
336		difss 4083	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∖ (𝑔 “ ℎ)) ⊆ 𝑏
337		xpss2 5671	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∖ (𝑔 “ ℎ)) ⊆ 𝑏 → ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) ⊆ ((𝑓 ∖ ℎ) × 𝑏))
338	336, 337	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) ⊆ ((𝑓 ∖ ℎ) × 𝑏)
339	335, 338	sstri 3940	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ ((𝑓 ∖ ℎ) × 𝑏)
340	45	inex1 5277	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ V
341	340	elpw 4561	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏) ↔ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ ((𝑓 ∖ ℎ) × 𝑏))
342	339, 341	mpbir 234	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)
343		incom 4155	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∩ ℎ) = (ℎ ∩ 𝑓)
344		dfss2 3917	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ⊆ 𝑓 ↔ (ℎ ∩ 𝑓) = ℎ)
345	220, 344	sylib 221	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ⊊ 𝑓 → (ℎ ∩ 𝑓) = ℎ)
346	343, 345	eqtrid 2808	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ ⊊ 𝑓 → (𝑓 ∩ ℎ) = ℎ)
347	346	neeq1d 3015	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ ⊊ 𝑓 → ((𝑓 ∩ ℎ) ≠ ∅ ↔ ℎ ≠ ∅))
348	347	biimpar 483	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → (𝑓 ∩ ℎ) ≠ ∅)
349		disj4 4412	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 ∩ ℎ) = ∅ ↔ ¬ (𝑓 ∖ ℎ) ⊊ 𝑓)
350	349	bicomi 227	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝑓 ∖ ℎ) ⊊ 𝑓 ↔ (𝑓 ∩ ℎ) = ∅)
351	350	necon1abii 3004	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∩ ℎ) ≠ ∅ ↔ (𝑓 ∖ ℎ) ⊊ 𝑓)
352	348, 351	sylib 221	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → (𝑓 ∖ ℎ) ⊊ 𝑓)
353	352	ad2antrl 741	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (𝑓 ∖ ℎ) ⊊ 𝑓)
354	128	difexi 5292	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∖ ℎ) ∈ V
355		psseq1 4038	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (𝑎 ⊊ 𝑓 ↔ (𝑓 ∖ ℎ) ⊊ 𝑓))
356		xpeq1 5665	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (𝑎 × 𝑏) = ((𝑓 ∖ ℎ) × 𝑏))
357	356	pweqd 4574	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (𝑓 ∖ ℎ) → 𝒫 (𝑎 × 𝑏) = 𝒫 ((𝑓 ∖ ℎ) × 𝑏))
358		pweq 4571	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (𝑓 ∖ ℎ) → 𝒫 𝑎 = 𝒫 (𝑓 ∖ ℎ))
359	358	raleqdv 3320	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑)))
360		f1eq2 6774	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (𝑒:𝑎–1-1→V ↔ 𝑒:(𝑓 ∖ ℎ)–1-1→V))
361	360	rexbidv 3187	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V))
362	359, 361	imbi12d 347	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (𝑓 ∖ ℎ) → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)))
363	357, 362	raleqbidv 3335	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)))
364	355, 363	imbi12d 347	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑓 ∖ ℎ) → ((𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ ((𝑓 ∖ ℎ) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V))))
365	354, 364	spcv 3560	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → ((𝑓 ∖ ℎ) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)))
366	239, 353, 365	sylc 66	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V))
367		imaeq1 6047	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (𝑐 “ 𝑑) = ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
368	367	breq2d 5115	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (𝑑 ≼ (𝑐 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑)))
369	368	ralbidv 3186	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑)))
370		pweq 4571	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝒫 𝑐 = 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))))
371	370	rexeqdv 3321	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V))
372	369, 371	imbi12d 347	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → ((∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V)))
373	372	rspcva 3575	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V))
374	342, 366, 373	sylancr 599	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V))
375	334, 374	mpd 16	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V)
376		f1eq1 6773	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑗 → (𝑒:(𝑓 ∖ ℎ)–1-1→V ↔ 𝑗:(𝑓 ∖ ℎ)–1-1→V))
377	376	cbvrexvw 3242	. . . . . . . . . . . . . . 15 ⊢ (∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V ↔ ∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V)
378	375, 377	sylib 221	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V)
379		elpwi 4564	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → 𝑖 ⊆ (𝑔 ↾ ℎ))
380		resss 5992	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ↾ ℎ) ⊆ 𝑔
381	379, 380	sstrdi 3943	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → 𝑖 ⊆ 𝑔)
382	381	adantr 486	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V) → 𝑖 ⊆ 𝑔)
383	382	ad2antlr 740	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑖 ⊆ 𝑔)
384		elpwi 4564	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝑗 ⊆ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))))
385		inss1 4182	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ 𝑔
386	384, 385	sstrdi 3943	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝑗 ⊆ 𝑔)
387	386	ad2antrl 741	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑗 ⊆ 𝑔)
388	383, 387	unssd 4138	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗) ⊆ 𝑔)
389	45	elpw2 5296	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∪ 𝑗) ∈ 𝒫 𝑔 ↔ (𝑖 ∪ 𝑗) ⊆ 𝑔)
390	388, 389	sylibr 237	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗) ∈ 𝒫 𝑔)
391		f1f1orn 6836	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖:ℎ–1-1→V → 𝑖:ℎ–1-1-onto→ran 𝑖)
392	391	adantl 487	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V) → 𝑖:ℎ–1-1-onto→ran 𝑖)
393	392	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑖:ℎ–1-1-onto→ran 𝑖)
394		f1f1orn 6836	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗:(𝑓 ∖ ℎ)–1-1→V → 𝑗:(𝑓 ∖ ℎ)–1-1-onto→ran 𝑗)
395	394	ad2antll 742	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑗:(𝑓 ∖ ℎ)–1-1-onto→ran 𝑗)
396		disjdif 4426	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ∩ (𝑓 ∖ ℎ)) = ∅
397	396	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ℎ ∩ (𝑓 ∖ ℎ)) = ∅)
398		rnss 5921	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ⊆ (𝑔 ↾ ℎ) → ran 𝑖 ⊆ ran (𝑔 ↾ ℎ))
399	379, 398	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → ran 𝑖 ⊆ ran (𝑔 ↾ ℎ))
400		df-ima 5664	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔 “ ℎ) = ran (𝑔 ↾ ℎ)
401	399, 400	sseqtrrdi 3972	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → ran 𝑖 ⊆ (𝑔 “ ℎ))
402	401	adantr 486	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V) → ran 𝑖 ⊆ (𝑔 “ ℎ))
403	402	ad2antlr 740	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ran 𝑖 ⊆ (𝑔 “ ℎ))
404		incom 4155	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 “ ℎ) ∩ ran 𝑗) = (ran 𝑗 ∩ (𝑔 “ ℎ))
405	384, 335	sstrdi 3943	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝑗 ⊆ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))
406		rnss 5921	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ⊆ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) → ran 𝑗 ⊆ ran ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))
407	405, 406	syl 18	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → ran 𝑗 ⊆ ran ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))
408		rnxpss 6164	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ran ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) ⊆ (𝑏 ∖ (𝑔 “ ℎ))
409	407, 408	sstrdi 3943	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → ran 𝑗 ⊆ (𝑏 ∖ (𝑔 “ ℎ)))
410	409	ad2antrl 741	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ran 𝑗 ⊆ (𝑏 ∖ (𝑔 “ ℎ)))
411		disjdifr 4427	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∖ (𝑔 “ ℎ)) ∩ (𝑔 “ ℎ)) = ∅
412		ssdisj 4413	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ran 𝑗 ⊆ (𝑏 ∖ (𝑔 “ ℎ)) ∧ ((𝑏 ∖ (𝑔 “ ℎ)) ∩ (𝑔 “ ℎ)) = ∅) → (ran 𝑗 ∩ (𝑔 “ ℎ)) = ∅)
413	410, 411, 412	sylancl 598	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ran 𝑗 ∩ (𝑔 “ ℎ)) = ∅)
414	404, 413	eqtrid 2808	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ((𝑔 “ ℎ) ∩ ran 𝑗) = ∅)
415		ssdisj 4413	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ran 𝑖 ⊆ (𝑔 “ ℎ) ∧ ((𝑔 “ ℎ) ∩ ran 𝑗) = ∅) → (ran 𝑖 ∩ ran 𝑗) = ∅)
416	403, 414, 415	syl2anc 596	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ran 𝑖 ∩ ran 𝑗) = ∅)
417		f1oun 6844	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑖:ℎ–1-1-onto→ran 𝑖 ∧ 𝑗:(𝑓 ∖ ℎ)–1-1-onto→ran 𝑗) ∧ ((ℎ ∩ (𝑓 ∖ ℎ)) = ∅ ∧ (ran 𝑖 ∩ ran 𝑗) = ∅)) → (𝑖 ∪ 𝑗):(ℎ ∪ (𝑓 ∖ ℎ))–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
418	393, 395, 397, 416, 417	syl22anc 852	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):(ℎ ∪ (𝑓 ∖ ℎ))–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
419		undif 4438	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ⊆ 𝑓 ↔ (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
420	419	bilani 510	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) → (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
421	420	ad2antrr 739	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
422	421	f1oeq2d 6820	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ((𝑖 ∪ 𝑗):(ℎ ∪ (𝑓 ∖ ℎ))–1-1-onto→(ran 𝑖 ∪ ran 𝑗) ↔ (𝑖 ∪ 𝑗):𝑓–1-1-onto→(ran 𝑖 ∪ ran 𝑗)))
423	418, 422	mpbid 235	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):𝑓–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
424		f1of1 6823	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∪ 𝑗):𝑓–1-1-onto→(ran 𝑖 ∪ ran 𝑗) → (𝑖 ∪ 𝑗):𝑓–1-1→(ran 𝑖 ∪ ran 𝑗))
425	423, 424	syl 18	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):𝑓–1-1→(ran 𝑖 ∪ ran 𝑗))
426		ssv 3955	. . . . . . . . . . . . . . . . . . 19 ⊢ (ran 𝑖 ∪ ran 𝑗) ⊆ V
427		f1ss 6785	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∪ 𝑗):𝑓–1-1→(ran 𝑖 ∪ ran 𝑗) ∧ (ran 𝑖 ∪ ran 𝑗) ⊆ V) → (𝑖 ∪ 𝑗):𝑓–1-1→V)
428	425, 426, 427	sylancl 598	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):𝑓–1-1→V)
429		f1eq1 6773	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖 ∪ 𝑗) → (𝑒:𝑓–1-1→V ↔ (𝑖 ∪ 𝑗):𝑓–1-1→V))
430	429	rspcev 3577	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∪ 𝑗) ∈ 𝒫 𝑔 ∧ (𝑖 ∪ 𝑗):𝑓–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
431	390, 428, 430	syl2anc 596	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
432	431	rexlimdvaa 3165	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
433	432	rexlimdvaa 3165	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) → (∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
434	252, 221, 433	syl2anc 596	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
435	272, 378, 434	mp2d 50	. . . . . . . . . . . . 13 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
436	435	ex 418	. . . . . . . . . . . 12 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
437	436	exlimdv 1966	. . . . . . . . . . 11 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (∃ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
438	437	imp 412	. . . . . . . . . 10 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∃ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
439	218, 438	sylan2br 607	. . . . . . . . 9 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ¬ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
440	217, 439	pm2.61dan 825	. . . . . . . 8 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
441	440	exp32 426	. . . . . . 7 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
442	441	ralrimiv 3154	. . . . . 6 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → ∀𝑔 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
443		imaeq1 6047	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → (𝑔 “ 𝑑) = (𝑐 “ 𝑑))
444	443	breq2d 5115	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → (𝑑 ≼ (𝑔 “ 𝑑) ↔ 𝑑 ≼ (𝑐 “ 𝑑)))
445	444	ralbidv 3186	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑)))
446		pweq 4571	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → 𝒫 𝑔 = 𝒫 𝑐)
447	446	rexeqdv 3321	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
448	445, 447	imbi12d 347	. . . . . . 7 ⊢ (𝑔 = 𝑐 → ((∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V)))
449	448	cbvralvw 3241	. . . . . 6 ⊢ (∀𝑔 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
450	442, 449	sylib 221	. . . . 5 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
451	450	exp31 425	. . . 4 ⊢ (𝑓 ∈ Fin → (𝑏 ∈ Fin → (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
452	451	a2d 30	. . 3 ⊢ (𝑓 ∈ Fin → ((𝑏 ∈ Fin → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
453	22, 452	biimtrid 245	. 2 ⊢ (𝑓 ∈ Fin → (∀𝑎(𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
454	9, 18, 453	findcard3 9274	1 ⊢ (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∧ wa 401  ∀wal 1568   = wceq 1570  ∃wex 1812   ∈ wcel 2145   ≠ wne 2956  ∀wral 3077  ∃wrex 3087  Vcvv 3451   ∖ cdif 3896   ∪ cun 3897   ∩ cin 3898   ⊆ wss 3899   ⊊ wpss 3900  ∅c0 4279  𝒫 cpw 4557  {csn 4584  ⟨cop 4590   class class class wbr 5103   × cxp 5649  ran crn 5652   ↾ cres 5653   “ cima 5654  –1-1→wf1 6535  –1-1-onto→wf1o 6537   ≈ cen 8970   ≼ cdom 8971   ≺ csdm 8972  Fincfn 8973

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2733  ax-sep 5249  ax-nul 5260  ax-pow 5327  ax-pr 5391  ax-un 7751

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3or 1104  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2100  df-mo 2565  df-eu 2595  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3078  df-rex 3088  df-reu 3367  df-rab 3414  df-v 3453  df-sbc 3740  df-csb 3848  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-pss 3919  df-nul 4280  df-if 4483  df-pw 4559  df-sn 4585  df-pr 4587  df-op 4591  df-uni 4868  df-br 5104  df-opab 5168  df-mpt 5187  df-tr 5213  df-id 5546  df-eprel 5551  df-po 5559  df-so 5560  df-fr 5604  df-we 5606  df-xp 5657  df-rel 5658  df-cnv 5659  df-co 5660  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664  df-ord 6365  df-on 6366  df-lim 6367  df-suc 6368  df-iota 6494  df-fun 6540  df-fn 6541  df-f 6542  df-f1 6543  df-fo 6544  df-f1o 6545  df-fv 6546  df-om 7878  df-1o 8476  df-er 8717  df-en 8974  df-dom 8975  df-sdom 8976  df-fin 8977

This theorem is used by:  marypha1  9426