Theorem marypha1lem 8627

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 5369	. . . . 5 ⊢ (𝑎 = 𝑓 → (𝑎 × 𝑏) = (𝑓 × 𝑏))
2	1	pweqd 4384	. . . 4 ⊢ (𝑎 = 𝑓 → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝑓 × 𝑏))
3		pweq 4382	. . . . . 6 ⊢ (𝑎 = 𝑓 → 𝒫 𝑎 = 𝒫 𝑓)
4	3	raleqdv 3340	. . . . 5 ⊢ (𝑎 = 𝑓 → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑)))
5		f1eq2 6347	. . . . . 6 ⊢ (𝑎 = 𝑓 → (𝑒:𝑎–1-1→V ↔ 𝑒:𝑓–1-1→V))
6	5	rexbidv 3237	. . . . 5 ⊢ (𝑎 = 𝑓 → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
7	4, 6	imbi12d 336	. . . 4 ⊢ (𝑎 = 𝑓 → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V)))
8	2, 7	raleqbidv 3326	. . 3 ⊢ (𝑎 = 𝑓 → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V)))
9	8	imbi2d 332	. 2 ⊢ (𝑎 = 𝑓 → ((𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
10		xpeq1 5369	. . . . 5 ⊢ (𝑎 = 𝐴 → (𝑎 × 𝑏) = (𝐴 × 𝑏))
11	10	pweqd 4384	. . . 4 ⊢ (𝑎 = 𝐴 → 𝒫 (𝑎 × 𝑏) = 𝒫 (𝐴 × 𝑏))
12		pweq 4382	. . . . . 6 ⊢ (𝑎 = 𝐴 → 𝒫 𝑎 = 𝒫 𝐴)
13	12	raleqdv 3340	. . . . 5 ⊢ (𝑎 = 𝐴 → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑)))
14		f1eq2 6347	. . . . . 6 ⊢ (𝑎 = 𝐴 → (𝑒:𝑎–1-1→V ↔ 𝑒:𝐴–1-1→V))
15	14	rexbidv 3237	. . . . 5 ⊢ (𝑎 = 𝐴 → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V))
16	13, 15	imbi12d 336	. . . 4 ⊢ (𝑎 = 𝐴 → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))
17	11, 16	raleqbidv 3326	. . 3 ⊢ (𝑎 = 𝐴 → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))
18	17	imbi2d 332	. 2 ⊢ (𝑎 = 𝐴 → ((𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V))))
19		bi2.04 379	. . . . 5 ⊢ ((𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ (𝑏 ∈ Fin → (𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
20	19	albii 1863	. . . 4 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ ∀𝑎(𝑏 ∈ Fin → (𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
21		19.21v 1982	. . . 4 ⊢ (∀𝑎(𝑏 ∈ Fin → (𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ (𝑏 ∈ Fin → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
22	20, 21	bitri 267	. . 3 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ↔ (𝑏 ∈ Fin → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))))
23		0elpw 5068	. . . . . . . . . . . . 13 ⊢ ∅ ∈ 𝒫 𝑔
24		f10 6423	. . . . . . . . . . . . 13 ⊢ ∅:∅–1-1→V
25		f1eq1 6346	. . . . . . . . . . . . . 14 ⊢ (𝑒 = ∅ → (𝑒:∅–1-1→V ↔ ∅:∅–1-1→V))
26	25	rspcev 3511	. . . . . . . . . . . . 13 ⊢ ((∅ ∈ 𝒫 𝑔 ∧ ∅:∅–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V)
27	23, 24, 26	mp2an 682	. . . . . . . . . . . 12 ⊢ ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V
28		f1eq2 6347	. . . . . . . . . . . . 13 ⊢ (𝑓 = ∅ → (𝑒:𝑓–1-1→V ↔ 𝑒:∅–1-1→V))
29	28	rexbidv 3237	. . . . . . . . . . . 12 ⊢ (𝑓 = ∅ → (∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑔𝑒:∅–1-1→V))
30	27, 29	mpbiri 250	. . . . . . . . . . 11 ⊢ (𝑓 = ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
31	30	a1i 11	. . . . . . . . . 10 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑓 = ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
32		n0 4159	. . . . . . . . . . 11 ⊢ (𝑓 ≠ ∅ ↔ ∃𝑖 𝑖 ∈ 𝑓)
33		snelpwi 5144	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑖 ∈ 𝑓 → {𝑖} ∈ 𝒫 𝑓)
34		id 22	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑖} → 𝑑 = {𝑖})
35		imaeq2 5716	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑑 = {𝑖} → (𝑔 “ 𝑑) = (𝑔 “ {𝑖}))
36	34, 35	breq12d 4899	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑑 = {𝑖} → (𝑑 ≼ (𝑔 “ 𝑑) ↔ {𝑖} ≼ (𝑔 “ {𝑖})))
37	36	rspcva 3509	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (({𝑖} ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → {𝑖} ≼ (𝑔 “ {𝑖}))
38		vex 3401	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑖 ∈ V
39	38	snnz 4542	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ {𝑖} ≠ ∅
40		snex 5140	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ {𝑖} ∈ V
41	40	0sdom 8379	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (∅ ≺ {𝑖} ↔ {𝑖} ≠ ∅)
42	39, 41	mpbir 223	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ∅ ≺ {𝑖}
43		sdomdomtr 8381	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((∅ ≺ {𝑖} ∧ {𝑖} ≼ (𝑔 “ {𝑖})) → ∅ ≺ (𝑔 “ {𝑖}))
44	42, 43	mpan 680	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ({𝑖} ≼ (𝑔 “ {𝑖}) → ∅ ≺ (𝑔 “ {𝑖}))
45		vex 3401	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ 𝑔 ∈ V
46	45	imaex 7383	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 “ {𝑖}) ∈ V
47	46	0sdom 8379	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (∅ ≺ (𝑔 “ {𝑖}) ↔ (𝑔 “ {𝑖}) ≠ ∅)
48	44, 47	sylib 210	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ({𝑖} ≼ (𝑔 “ {𝑖}) → (𝑔 “ {𝑖}) ≠ ∅)
49	37, 48	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (({𝑖} ∈ 𝒫 𝑓 ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → (𝑔 “ {𝑖}) ≠ ∅)
50	49	expcom 404	. . . . . . . . . . . . . . . . . . 19 ⊢ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ({𝑖} ∈ 𝒫 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
51	33, 50	syl5 34	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → (𝑖 ∈ 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
52	51	adantl 475	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → (𝑖 ∈ 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
53	52	ad2antlr 717	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑖 ∈ 𝑓 → (𝑔 “ {𝑖}) ≠ ∅))
54	53	impr 448	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → (𝑔 “ {𝑖}) ≠ ∅)
55		n0 4159	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 “ {𝑖}) ≠ ∅ ↔ ∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}))
56	54, 55	sylib 210	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → ∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}))
57	45	imaex 7383	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 “ 𝑐) ∈ V
58	57	difexi 5046	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 “ 𝑐) ∖ {𝑗}) ∈ V
59	58	0dom 8378	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ∅ ≼ ((𝑔 “ 𝑐) ∖ {𝑗})
60		breq1 4889	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 = ∅ → (𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}) ↔ ∅ ≼ ((𝑔 “ 𝑐) ∖ {𝑗})))
61	59, 60	mpbiri 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 = ∅ → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
62	61	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → (𝑐 = ∅ → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗})))
63		simpll 757	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)))
64		elpwi 4389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → 𝑐 ⊆ (𝑓 ∖ {𝑖}))
65	64	ad2antrl 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ⊆ (𝑓 ∖ {𝑖}))
66		difsnpss 4569	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑖 ∈ 𝑓 ↔ (𝑓 ∖ {𝑖}) ⊊ 𝑓)
67	66	biimpi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑖 ∈ 𝑓 → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
68	67	ad2antlr 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
69	65, 68	sspsstrd 3937	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ⊊ 𝑓)
70		simprr 763	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≠ ∅)
71	69, 70	jca 507	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → (𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅))
72		psseq1 3916	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → (ℎ ⊊ 𝑓 ↔ 𝑐 ⊊ 𝑓))
73		neeq1 3031	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → (ℎ ≠ ∅ ↔ 𝑐 ≠ ∅))
74	72, 73	anbi12d 624	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (ℎ = 𝑐 → ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ↔ (𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅)))
75		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → ℎ = 𝑐)
76		imaeq2 5716	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (ℎ = 𝑐 → (𝑔 “ ℎ) = (𝑔 “ 𝑐))
77	75, 76	breq12d 4899	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (ℎ = 𝑐 → (ℎ ≺ (𝑔 “ ℎ) ↔ 𝑐 ≺ (𝑔 “ 𝑐)))
78	74, 77	imbi12d 336	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (ℎ = 𝑐 → (((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ↔ ((𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅) → 𝑐 ≺ (𝑔 “ 𝑐))))
79	78	spv 2358	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) → ((𝑐 ⊊ 𝑓 ∧ 𝑐 ≠ ∅) → 𝑐 ≺ (𝑔 “ 𝑐)))
80	63, 71, 79	sylc 65	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≺ (𝑔 “ 𝑐))
81		domdifsn 8331	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 ≺ (𝑔 “ 𝑐) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
82	80, 81	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) ∧ 𝑐 ≠ ∅)) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
83	82	expr 450	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → (𝑐 ≠ ∅ → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗})))
84	62, 83	pm2.61dne 3056	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
85	84	adantlrr 711	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
86	85	adantll 704	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ {𝑗}))
87		df-ss 3806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑐 ⊆ (𝑓 ∖ {𝑖}) ↔ (𝑐 ∩ (𝑓 ∖ {𝑖})) = 𝑐)
88	64, 87	sylib 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → (𝑐 ∩ (𝑓 ∖ {𝑖})) = 𝑐)
89	88	imaeq2d 5720	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → (𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) = (𝑔 “ 𝑐))
90	89	ineq1d 4036	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖}) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})))
91	90	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})))
92		indif2 4097	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ {𝑗})
93		imassrn 5731	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 “ 𝑐) ⊆ ran 𝑔
94		elpwi 4389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → 𝑔 ⊆ (𝑓 × 𝑏))
95		rnss 5599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → ran 𝑔 ⊆ ran (𝑓 × 𝑏))
96		rnxpss 5820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ran (𝑓 × 𝑏) ⊆ 𝑏
97	95, 96	syl6ss 3833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → ran 𝑔 ⊆ 𝑏)
98	94, 97	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ran 𝑔 ⊆ 𝑏)
99	93, 98	syl5ss 3832	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔 “ 𝑐) ⊆ 𝑏)
100		df-ss 3806	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 “ 𝑐) ⊆ 𝑏 ↔ ((𝑔 “ 𝑐) ∩ 𝑏) = (𝑔 “ 𝑐))
101	99, 100	sylib 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ((𝑔 “ 𝑐) ∩ 𝑏) = (𝑔 “ 𝑐))
102	101	difeq1d 3950	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ {𝑗}) = ((𝑔 “ 𝑐) ∖ {𝑗}))
103	102	ad2antrl 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ {𝑗}) = ((𝑔 “ 𝑐) ∖ {𝑗}))
104	92, 103	syl5eq 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∖ {𝑗}))
105	104	ad2antrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ 𝑐) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∖ {𝑗}))
106	91, 105	eqtrd 2814	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 “ 𝑐) ∖ {𝑗}))
107	86, 106	breqtrrd 4914	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})) → 𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})))
108	107	ralrimiva 3148	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})))
109		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑑 → 𝑐 = 𝑑)
110		imainrect 5829	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑐) = ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗}))
111		imaeq2 5716	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = 𝑑 → ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑐) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
112	110, 111	syl5eqr 2828	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = 𝑑 → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
113	109, 112	breq12d 4899	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = 𝑑 → (𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
114	113	cbvralv 3367	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑐 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ {𝑖}))) ∩ (𝑏 ∖ {𝑗})) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
115	108, 114	sylib 210	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
116	115	adantllr 709	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
117		inss2 4054	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))
118		difss 3960	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑏 ∖ {𝑗}) ⊆ 𝑏
119		xpss2 5375	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∖ {𝑗}) ⊆ 𝑏 → ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏))
120	118, 119	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏)
121	117, 120	sstri 3830	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏)
122	45	inex1 5036	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ V
123	122	elpw 4385	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏) ↔ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ ((𝑓 ∖ {𝑖}) × 𝑏))
124	121, 123	mpbir 223	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)
125		simpllr 766	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)))
126	67	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
127	126	ad2antll 719	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (𝑓 ∖ {𝑖}) ⊊ 𝑓)
128		vex 3401	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ 𝑓 ∈ V
129	128	difexi 5046	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 ∖ {𝑖}) ∈ V
130		psseq1 3916	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (𝑎 ⊊ 𝑓 ↔ (𝑓 ∖ {𝑖}) ⊊ 𝑓))
131		xpeq1 5369	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (𝑎 × 𝑏) = ((𝑓 ∖ {𝑖}) × 𝑏))
132	131	pweqd 4384	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → 𝒫 (𝑎 × 𝑏) = 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏))
133		pweq 4382	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → 𝒫 𝑎 = 𝒫 (𝑓 ∖ {𝑖}))
134	133	raleqdv 3340	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑)))
135		f1eq2 6347	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (𝑒:𝑎–1-1→V ↔ 𝑒:(𝑓 ∖ {𝑖})–1-1→V))
136	135	rexbidv 3237	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))
137	134, 136	imbi12d 336	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
138	132, 137	raleqbidv 3326	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
139	130, 138	imbi12d 336	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑎 = (𝑓 ∖ {𝑖}) → ((𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ ((𝑓 ∖ {𝑖}) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))))
140	129, 139	spcv 3501	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → ((𝑓 ∖ {𝑖}) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
141	125, 127, 140	sylc 65	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V))
142		imaeq1 5715	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (𝑐 “ 𝑑) = ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑))
143	142	breq2d 4898	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (𝑑 ≼ (𝑐 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
144	143	ralbidv 3168	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑)))
145		pweq 4382	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝒫 𝑐 = 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))))
146	145	rexeqdv 3341	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
147	144, 146	imbi12d 336	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ((∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V)))
148	147	rspcva 3509	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ {𝑖}) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ {𝑖})–1-1→V)) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ {𝑖})𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V))
149	124, 141, 148	sylancr 581	. . . . . . . . . . . . . . . . . . . . 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 6346	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑒 = 𝑘 → (𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ 𝑘:(𝑓 ∖ {𝑖})–1-1→V))
152	151	cbvrexv 3368	. . . . . . . . . . . . . . . . . . . 20 ⊢ (∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑒:(𝑓 ∖ {𝑖})–1-1→V ↔ ∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V)
153	150, 152	sylib 210	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V)
154		vex 3401	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ 𝑗 ∈ V
155	38, 154	elimasn 5744	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑗 ∈ (𝑔 “ {𝑖}) ↔ ⟨𝑖, 𝑗⟩ ∈ 𝑔)
156	155	biimpi 208	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑗 ∈ (𝑔 “ {𝑖}) → ⟨𝑖, 𝑗⟩ ∈ 𝑔)
157	156	snssd 4571	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑗 ∈ (𝑔 “ {𝑖}) → {⟨𝑖, 𝑗⟩} ⊆ 𝑔)
158	157	ad2antlr 717	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → {⟨𝑖, 𝑗⟩} ⊆ 𝑔)
159		elpwi 4389	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))))
160		inss1 4053	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ⊆ 𝑔
161	159, 160	syl6ss 3833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ 𝑔)
162	161	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → 𝑘 ⊆ 𝑔)
163	158, 162	unssd 4012	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ⊆ 𝑔)
164	45	elpw2 5062	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔 ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ⊆ 𝑔)
165	163, 164	sylibr 226	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) ∧ 𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔)
166	165	ad2ant2lr 738	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔)
167	38, 154	f1osn 6430	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ {⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗}
168	167	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → {⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗})
169		f1f1orn 6402	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘:(𝑓 ∖ {𝑖})–1-1→V → 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘)
170	169	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘)
171		disjdif 4264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅
172	171	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅)
173		incom 4028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ ({𝑗} ∩ ran 𝑘) = (ran 𝑘 ∩ {𝑗})
174	159, 117	syl6ss 3833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → 𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))
175		rnss 5599	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ (𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) → ran 𝑘 ⊆ ran ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))
176		rnxpss 5820	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ⊢ ran ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) ⊆ (𝑏 ∖ {𝑗})
177	175, 176	syl6ss 3833	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ (𝑘 ⊆ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})) → ran 𝑘 ⊆ (𝑏 ∖ {𝑗}))
178	174, 177	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ran 𝑘 ⊆ (𝑏 ∖ {𝑗}))
179		incom 4028	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ({𝑗} ∩ (𝑏 ∖ {𝑗}))
180		disjdif 4264	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ⊢ ({𝑗} ∩ (𝑏 ∖ {𝑗})) = ∅
181	179, 180	eqtri 2802	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ∅
182		ssdisj 4252	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ⊢ ((ran 𝑘 ⊆ (𝑏 ∖ {𝑗}) ∧ ((𝑏 ∖ {𝑗}) ∩ {𝑗}) = ∅) → (ran 𝑘 ∩ {𝑗}) = ∅)
183	178, 181, 182	sylancl 580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → (ran 𝑘 ∩ {𝑗}) = ∅)
184	173, 183	syl5eq 2826	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) → ({𝑗} ∩ ran 𝑘) = ∅)
185	184	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({𝑗} ∩ ran 𝑘) = ∅)
186		f1oun 6410	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((({⟨𝑖, 𝑗⟩}:{𝑖}–1-1-onto→{𝑗} ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1-onto→ran 𝑘) ∧ (({𝑖} ∩ (𝑓 ∖ {𝑖})) = ∅ ∧ ({𝑗} ∩ ran 𝑘) = ∅)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
187	168, 170, 172, 185, 186	syl22anc 829	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
188	187	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘))
189		snssi 4570	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ⊢ (𝑖 ∈ 𝑓 → {𝑖} ⊆ 𝑓)
190	189	ad2antrl 718	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → {𝑖} ⊆ 𝑓)
191		undif 4273	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ⊢ ({𝑖} ⊆ 𝑓 ↔ ({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓)
192	190, 191	sylib 210	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → ({𝑖} ∪ (𝑓 ∖ {𝑖})) = 𝑓)
193	192	f1oeq2d 6387	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘)))
194	193	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → (({⟨𝑖, 𝑗⟩} ∪ 𝑘):({𝑖} ∪ (𝑓 ∖ {𝑖}))–1-1-onto→({𝑗} ∪ ran 𝑘) ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘)))
195	188, 194	mpbid 224	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘))
196		f1of1 6390	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→({𝑗} ∪ ran 𝑘))
197		ssv 3844	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ({𝑗} ∪ ran 𝑘) ⊆ V
198		f1ss 6356	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ((({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→({𝑗} ∪ ran 𝑘) ∧ ({𝑗} ∪ ran 𝑘) ⊆ V) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V)
199	196, 197, 198	sylancl 580	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1-onto→({𝑗} ∪ ran 𝑘) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V)
200	195, 199	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V)
201		f1eq1 6346	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑒 = ({⟨𝑖, 𝑗⟩} ∪ 𝑘) → (𝑒:𝑓–1-1→V ↔ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V))
202	201	rspcev 3511	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((({⟨𝑖, 𝑗⟩} ∪ 𝑘) ∈ 𝒫 𝑔 ∧ ({⟨𝑖, 𝑗⟩} ∪ 𝑘):𝑓–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
203	166, 200, 202	syl2anc 579	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) ∧ (𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗}))) ∧ 𝑘:(𝑓 ∖ {𝑖})–1-1→V)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
204	203	rexlimdvaa 3214	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖}))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
205	204	ex 403	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
206	205	adantr 474	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑)) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
207	206	ad2antlr 717	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
208	207	impr 448	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
209	208	adantllr 709	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → (∃𝑘 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ {𝑖}) × (𝑏 ∖ {𝑗})))𝑘:(𝑓 ∖ {𝑖})–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
210	153, 209	mpd 15	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ (𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
211	210	expr 450	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ((𝑖 ∈ 𝑓 ∧ 𝑗 ∈ (𝑔 “ {𝑖})) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
212	211	expd 406	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑖 ∈ 𝑓 → (𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
213	212	impr 448	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → (𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
214	213	exlimdv 1976	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → (∃𝑗 𝑗 ∈ (𝑔 “ {𝑖}) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
215	56, 214	mpd 15	. . . . . . . . . . . . 13 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ (∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)) ∧ 𝑖 ∈ 𝑓)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
216	215	expr 450	. . . . . . . . . . . 12 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑖 ∈ 𝑓 → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
217	216	exlimdv 1976	. . . . . . . . . . 11 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (∃𝑖 𝑖 ∈ 𝑓 → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
218	32, 217	syl5bi 234	. . . . . . . . . 10 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → (𝑓 ≠ ∅ → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
219	31, 218	pm2.61dne 3056	. . . . . . . . 9 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
220		exanali 1904	. . . . . . . . . 10 ⊢ (∃ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) ↔ ¬ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ)))
221		simprll 769	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ℎ ⊊ 𝑓)
222		pssss 3924	. . . . . . . . . . . . . . . . . . . 20 ⊢ (ℎ ⊊ 𝑓 → ℎ ⊆ 𝑓)
223	221, 222	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ℎ ⊆ 𝑓)
224		sspwb 5149	. . . . . . . . . . . . . . . . . . 19 ⊢ (ℎ ⊆ 𝑓 ↔ 𝒫 ℎ ⊆ 𝒫 𝑓)
225	223, 224	sylib 210	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → 𝒫 ℎ ⊆ 𝒫 𝑓)
226		simplrr 768	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))
227		ssralv 3885	. . . . . . . . . . . . . . . . . 18 ⊢ (𝒫 ℎ ⊆ 𝒫 𝑓 → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑔 “ 𝑑)))
228	225, 226, 227	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑔 “ 𝑑))
229		elpwi 4389	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ∈ 𝒫 ℎ → 𝑑 ⊆ ℎ)
230		resima2 5681	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑑 ⊆ ℎ → ((𝑔 ↾ ℎ) “ 𝑑) = (𝑔 “ 𝑑))
231	229, 230	syl 17	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑑 ∈ 𝒫 ℎ → ((𝑔 ↾ ℎ) “ 𝑑) = (𝑔 “ 𝑑))
232	231	eqcomd 2784	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑑 ∈ 𝒫 ℎ → (𝑔 “ 𝑑) = ((𝑔 ↾ ℎ) “ 𝑑))
233	232	breq2d 4898	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑑 ∈ 𝒫 ℎ → (𝑑 ≼ (𝑔 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑)))
234	233	ralbiia 3161	. . . . . . . . . . . . . . . . 17 ⊢ (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑔 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑))
235	228, 234	sylib 210	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑))
236		imaeq1 5715	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (𝑐 “ 𝑑) = ((𝑔 ↾ ℎ) “ 𝑑))
237	236	breq2d 4898	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (𝑑 ≼ (𝑐 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑)))
238	237	ralbidv 3168	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑)))
239		pweq 4382	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ↾ ℎ) → 𝒫 𝑐 = 𝒫 (𝑔 ↾ ℎ))
240	239	rexeqdv 3341	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑔 ↾ ℎ) → (∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V))
241	238, 240	imbi12d 336	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = (𝑔 ↾ ℎ) → ((∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V) ↔ (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V)))
242		simpllr 766	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)))
243		psseq1 3916	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ℎ → (𝑎 ⊊ 𝑓 ↔ ℎ ⊊ 𝑓))
244		xpeq1 5369	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = ℎ → (𝑎 × 𝑏) = (ℎ × 𝑏))
245	244	pweqd 4384	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = ℎ → 𝒫 (𝑎 × 𝑏) = 𝒫 (ℎ × 𝑏))
246		pweq 4382	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = ℎ → 𝒫 𝑎 = 𝒫 ℎ)
247	246	raleqdv 3340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = ℎ → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑)))
248		f1eq2 6347	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = ℎ → (𝑒:𝑎–1-1→V ↔ 𝑒:ℎ–1-1→V))
249	248	rexbidv 3237	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = ℎ → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V))
250	247, 249	imbi12d 336	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = ℎ → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V)))
251	245, 250	raleqbidv 3326	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = ℎ → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V)))
252	243, 251	imbi12d 336	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = ℎ → ((𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ (ℎ ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V))))
253	252	spv 2358	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → (ℎ ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V)))
254	242, 221, 253	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑐 ∈ 𝒫 (ℎ × 𝑏)(∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:ℎ–1-1→V))
255		simplrl 767	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → 𝑔 ∈ 𝒫 (𝑓 × 𝑏))
256		ssres 5673	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ⊆ ((𝑓 × 𝑏) ↾ ℎ))
257		df-res 5367	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 × 𝑏) ↾ ℎ) = ((𝑓 × 𝑏) ∩ (ℎ × V))
258		inxp 5500	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 × 𝑏) ∩ (ℎ × V)) = ((𝑓 ∩ ℎ) × (𝑏 ∩ V))
259		inss2 4054	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑓 ∩ ℎ) ⊆ ℎ
260		inss1 4053	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑏 ∩ V) ⊆ 𝑏
261		xpss12 5370	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((𝑓 ∩ ℎ) ⊆ ℎ ∧ (𝑏 ∩ V) ⊆ 𝑏) → ((𝑓 ∩ ℎ) × (𝑏 ∩ V)) ⊆ (ℎ × 𝑏))
262	259, 260, 261	mp2an 682	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑓 ∩ ℎ) × (𝑏 ∩ V)) ⊆ (ℎ × 𝑏)
263	258, 262	eqsstri 3854	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 × 𝑏) ∩ (ℎ × V)) ⊆ (ℎ × 𝑏)
264	257, 263	eqsstri 3854	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑓 × 𝑏) ↾ ℎ) ⊆ (ℎ × 𝑏)
265	256, 264	syl6ss 3833	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ⊆ (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ⊆ (ℎ × 𝑏))
266	94, 265	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ⊆ (ℎ × 𝑏))
267	45	resex 5693	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑔 ↾ ℎ) ∈ V
268	267	elpw 4385	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑔 ↾ ℎ) ∈ 𝒫 (ℎ × 𝑏) ↔ (𝑔 ↾ ℎ) ⊆ (ℎ × 𝑏))
269	266, 268	sylibr 226	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (𝑔 ↾ ℎ) ∈ 𝒫 (ℎ × 𝑏))
270	255, 269	syl 17	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (𝑔 ↾ ℎ) ∈ 𝒫 (ℎ × 𝑏))
271	241, 254, 270	rspcdva 3517	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (∀𝑑 ∈ 𝒫 ℎ𝑑 ≼ ((𝑔 ↾ ℎ) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V))
272	235, 271	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V)
273		f1eq1 6346	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑖 → (𝑒:ℎ–1-1→V ↔ 𝑖:ℎ–1-1→V))
274	273	cbvrexv 3368	. . . . . . . . . . . . . . 15 ⊢ (∃𝑒 ∈ 𝒫 (𝑔 ↾ ℎ)𝑒:ℎ–1-1→V ↔ ∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V)
275	272, 274	sylib 210	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V)
276		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (ℎ ∪ 𝑐) → 𝑑 = (ℎ ∪ 𝑐))
277		imaeq2 5716	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑑 = (ℎ ∪ 𝑐) → (𝑔 “ 𝑑) = (𝑔 “ (ℎ ∪ 𝑐)))
278	276, 277	breq12d 4899	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑑 = (ℎ ∪ 𝑐) → (𝑑 ≼ (𝑔 “ 𝑑) ↔ (ℎ ∪ 𝑐) ≼ (𝑔 “ (ℎ ∪ 𝑐))))
279		simprr 763	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))
280	279	ad2antrr 716	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))
281	222	ad2antrr 716	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) → ℎ ⊆ 𝑓)
282	281	ad2antlr 717	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ⊆ 𝑓)
283		elpwi 4389	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → 𝑐 ⊆ (𝑓 ∖ ℎ))
284		difss 3960	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑓 ∖ ℎ) ⊆ 𝑓
285	283, 284	syl6ss 3833	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → 𝑐 ⊆ 𝑓)
286	285	adantl 475	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ⊆ 𝑓)
287	282, 286	unssd 4012	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ⊆ 𝑓)
288	128	elpw2 5062	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ℎ ∪ 𝑐) ∈ 𝒫 𝑓 ↔ (ℎ ∪ 𝑐) ⊆ 𝑓)
289	287, 288	sylibr 226	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ∈ 𝒫 𝑓)
290	278, 280, 289	rspcdva 3517	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ≼ (𝑔 “ (ℎ ∪ 𝑐)))
291		imaundi 5799	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑔 “ (ℎ ∪ 𝑐)) = ((𝑔 “ ℎ) ∪ (𝑔 “ 𝑐))
292		undif2 4268	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ((𝑔 “ ℎ) ∪ (𝑔 “ 𝑐))
293	291, 292	eqtr4i 2805	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 “ (ℎ ∪ 𝑐)) = ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
294	290, 293	syl6breq 4927	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∪ 𝑐) ≼ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))))
295		simp-4l 773	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑓 ∈ Fin)
296	295, 282	ssfid 8471	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ∈ Fin)
297		id 22	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 = ℎ → 𝑑 = ℎ)
298		imaeq2 5716	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑑 = ℎ → (𝑔 “ 𝑑) = (𝑔 “ ℎ))
299	297, 298	breq12d 4899	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑑 = ℎ → (𝑑 ≼ (𝑔 “ 𝑑) ↔ ℎ ≼ (𝑔 “ ℎ)))
300		vex 3401	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ ℎ ∈ V
301	300	elpw 4385	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (ℎ ∈ 𝒫 𝑓 ↔ ℎ ⊆ 𝑓)
302	282, 301	sylibr 226	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ∈ 𝒫 𝑓)
303	299, 280, 302	rspcdva 3517	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ≼ (𝑔 “ ℎ))
304		simplrr 768	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ¬ ℎ ≺ (𝑔 “ ℎ))
305		bren2 8272	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ ≈ (𝑔 “ ℎ) ↔ (ℎ ≼ (𝑔 “ ℎ) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)))
306	303, 304, 305	sylanbrc 578	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ℎ ≈ (𝑔 “ ℎ))
307	306	ensymd 8292	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (𝑔 “ ℎ) ≈ ℎ)
308		incom 4028	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (ℎ ∩ 𝑐) = (𝑐 ∩ ℎ)
309		ssdifin0 4274	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑐 ⊆ (𝑓 ∖ ℎ) → (𝑐 ∩ ℎ) = ∅)
310	308, 309	syl5eq 2826	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 ⊆ (𝑓 ∖ ℎ) → (ℎ ∩ 𝑐) = ∅)
311	283, 310	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → (ℎ ∩ 𝑐) = ∅)
312	311	adantl 475	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (ℎ ∩ 𝑐) = ∅)
313		disjdif 4264	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 “ ℎ) ∩ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ∅
314	313	a1i 11	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ((𝑔 “ ℎ) ∩ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ∅)
315		domunfican 8521	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (((ℎ ∈ Fin ∧ (𝑔 “ ℎ) ≈ ℎ) ∧ ((ℎ ∩ 𝑐) = ∅ ∧ ((𝑔 “ ℎ) ∩ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) = ∅)) → ((ℎ ∪ 𝑐) ≼ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) ↔ 𝑐 ≼ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))))
316	296, 307, 312, 314, 315	syl22anc 829	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ((ℎ ∪ 𝑐) ≼ ((𝑔 “ ℎ) ∪ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))) ↔ 𝑐 ≼ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ))))
317	294, 316	mpbid 224	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ≼ ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
318	101	difeq1d 3950	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)) = ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
319	318	ad2antrl 718	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)) = ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
320	319	ad2antrr 716	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)) = ((𝑔 “ 𝑐) ∖ (𝑔 “ ℎ)))
321	317, 320	breqtrrd 4914	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ≼ (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)))
322		df-ss 3806	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑐 ⊆ (𝑓 ∖ ℎ) ↔ (𝑐 ∩ (𝑓 ∖ ℎ)) = 𝑐)
323	283, 322	sylib 210	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → (𝑐 ∩ (𝑓 ∖ ℎ)) = 𝑐)
324	323	imaeq2d 5720	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → (𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) = (𝑔 “ 𝑐))
325	324	ineq1d 4036	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = ((𝑔 “ 𝑐) ∩ (𝑏 ∖ (𝑔 “ ℎ))))
326		indif2 4097	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑔 “ 𝑐) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ))
327	325, 326	syl6eq 2830	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 ∈ 𝒫 (𝑓 ∖ ℎ) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)))
328	327	adantl 475	. . . . . . . . . . . . . . . . . . . 20 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = (((𝑔 “ 𝑐) ∩ 𝑏) ∖ (𝑔 “ ℎ)))
329	321, 328	breqtrrd 4914	. . . . . . . . . . . . . . . . . . 19 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) ∧ 𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)) → 𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))))
330	329	ralrimiva 3148	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))))
331		imainrect 5829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑐) = ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ)))
332		imaeq2 5716	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = 𝑑 → ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑐) = ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
333	331, 332	syl5eqr 2828	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = 𝑑 → ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
334	109, 333	breq12d 4899	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = 𝑑 → (𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑)))
335	334	cbvralv 3367	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑐 ∈ 𝒫 (𝑓 ∖ ℎ)𝑐 ≼ ((𝑔 “ (𝑐 ∩ (𝑓 ∖ ℎ))) ∩ (𝑏 ∖ (𝑔 “ ℎ))) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
336	330, 335	sylib 210	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
337	336	adantllr 709	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
338		inss2 4054	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))
339		difss 3960	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑏 ∖ (𝑔 “ ℎ)) ⊆ 𝑏
340		xpss2 5375	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑏 ∖ (𝑔 “ ℎ)) ⊆ 𝑏 → ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) ⊆ ((𝑓 ∖ ℎ) × 𝑏))
341	339, 340	ax-mp 5	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) ⊆ ((𝑓 ∖ ℎ) × 𝑏)
342	338, 341	sstri 3830	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ ((𝑓 ∖ ℎ) × 𝑏)
343	45	inex1 5036	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ V
344	343	elpw 4385	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏) ↔ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ ((𝑓 ∖ ℎ) × 𝑏))
345	342, 344	mpbir 223	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)
346		incom 4028	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑓 ∩ ℎ) = (ℎ ∩ 𝑓)
347		df-ss 3806	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ⊆ 𝑓 ↔ (ℎ ∩ 𝑓) = ℎ)
348	222, 347	sylib 210	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ⊊ 𝑓 → (ℎ ∩ 𝑓) = ℎ)
349	346, 348	syl5eq 2826	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (ℎ ⊊ 𝑓 → (𝑓 ∩ ℎ) = ℎ)
350	349	neeq1d 3028	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (ℎ ⊊ 𝑓 → ((𝑓 ∩ ℎ) ≠ ∅ ↔ ℎ ≠ ∅))
351	350	biimpar 471	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → (𝑓 ∩ ℎ) ≠ ∅)
352		disj4 4251	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((𝑓 ∩ ℎ) = ∅ ↔ ¬ (𝑓 ∖ ℎ) ⊊ 𝑓)
353	352	bicomi 216	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (¬ (𝑓 ∖ ℎ) ⊊ 𝑓 ↔ (𝑓 ∩ ℎ) = ∅)
354	353	necon1abii 3017	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑓 ∩ ℎ) ≠ ∅ ↔ (𝑓 ∖ ℎ) ⊊ 𝑓)
355	351, 354	sylib 210	. . . . . . . . . . . . . . . . . . 19 ⊢ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → (𝑓 ∖ ℎ) ⊊ 𝑓)
356	355	ad2antrl 718	. . . . . . . . . . . . . . . . . 18 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (𝑓 ∖ ℎ) ⊊ 𝑓)
357	128	difexi 5046	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑓 ∖ ℎ) ∈ V
358		psseq1 3916	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (𝑎 ⊊ 𝑓 ↔ (𝑓 ∖ ℎ) ⊊ 𝑓))
359		xpeq1 5369	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (𝑎 × 𝑏) = ((𝑓 ∖ ℎ) × 𝑏))
360	359	pweqd 4384	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (𝑓 ∖ ℎ) → 𝒫 (𝑎 × 𝑏) = 𝒫 ((𝑓 ∖ ℎ) × 𝑏))
361		pweq 4382	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (𝑓 ∖ ℎ) → 𝒫 𝑎 = 𝒫 (𝑓 ∖ ℎ))
362	361	raleqdv 3340	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑)))
363		f1eq2 6347	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (𝑒:𝑎–1-1→V ↔ 𝑒:(𝑓 ∖ ℎ)–1-1→V))
364	363	rexbidv 3237	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V))
365	362, 364	imbi12d 336	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑎 = (𝑓 ∖ ℎ) → ((∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)))
366	360, 365	raleqbidv 3326	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑎 = (𝑓 ∖ ℎ) → (∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V) ↔ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)))
367	358, 366	imbi12d 336	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑎 = (𝑓 ∖ ℎ) → ((𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) ↔ ((𝑓 ∖ ℎ) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V))))
368	357, 367	spcv 3501	. . . . . . . . . . . . . . . . . 18 ⊢ (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → ((𝑓 ∖ ℎ) ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)))
369	242, 356, 368	sylc 65	. . . . . . . . . . . . . . . . 17 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V))
370		imaeq1 5715	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (𝑐 “ 𝑑) = ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑))
371	370	breq2d 4898	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (𝑑 ≼ (𝑐 “ 𝑑) ↔ 𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑)))
372	371	ralbidv 3168	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑)))
373		pweq 4382	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝒫 𝑐 = 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))))
374	373	rexeqdv 3341	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → (∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V ↔ ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V))
375	372, 374	imbi12d 336	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑐 = (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → ((∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V) ↔ (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V)))
376	375	rspcva 3509	. . . . . . . . . . . . . . . . 17 ⊢ (((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏) ∧ ∀𝑐 ∈ 𝒫 ((𝑓 ∖ ℎ) × 𝑏)(∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:(𝑓 ∖ ℎ)–1-1→V)) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V))
377	345, 369, 376	sylancr 581	. . . . . . . . . . . . . . . 16 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (∀𝑑 ∈ 𝒫 (𝑓 ∖ ℎ)𝑑 ≼ ((𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) “ 𝑑) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V))
378	337, 377	mpd 15	. . . . . . . . . . . . . . 15 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V)
379		f1eq1 6346	. . . . . . . . . . . . . . . 16 ⊢ (𝑒 = 𝑗 → (𝑒:(𝑓 ∖ ℎ)–1-1→V ↔ 𝑗:(𝑓 ∖ ℎ)–1-1→V))
380	379	cbvrexv 3368	. . . . . . . . . . . . . . 15 ⊢ (∃𝑒 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑒:(𝑓 ∖ ℎ)–1-1→V ↔ ∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V)
381	378, 380	sylib 210	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V)
382		elpwi 4389	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → 𝑖 ⊆ (𝑔 ↾ ℎ))
383		resss 5671	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑔 ↾ ℎ) ⊆ 𝑔
384	382, 383	syl6ss 3833	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → 𝑖 ⊆ 𝑔)
385	384	adantr 474	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V) → 𝑖 ⊆ 𝑔)
386	385	ad2antlr 717	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑖 ⊆ 𝑔)
387		elpwi 4389	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝑗 ⊆ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))))
388		inss1 4053	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ⊆ 𝑔
389	387, 388	syl6ss 3833	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝑗 ⊆ 𝑔)
390	389	ad2antrl 718	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑗 ⊆ 𝑔)
391	386, 390	unssd 4012	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗) ⊆ 𝑔)
392	45	elpw2 5062	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑖 ∪ 𝑗) ∈ 𝒫 𝑔 ↔ (𝑖 ∪ 𝑗) ⊆ 𝑔)
393	391, 392	sylibr 226	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗) ∈ 𝒫 𝑔)
394		f1f1orn 6402	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (𝑖:ℎ–1-1→V → 𝑖:ℎ–1-1-onto→ran 𝑖)
395	394	adantl 475	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V) → 𝑖:ℎ–1-1-onto→ran 𝑖)
396	395	ad2antlr 717	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑖:ℎ–1-1-onto→ran 𝑖)
397		f1f1orn 6402	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (𝑗:(𝑓 ∖ ℎ)–1-1→V → 𝑗:(𝑓 ∖ ℎ)–1-1-onto→ran 𝑗)
398	397	ad2antll 719	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → 𝑗:(𝑓 ∖ ℎ)–1-1-onto→ran 𝑗)
399		disjdif 4264	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (ℎ ∩ (𝑓 ∖ ℎ)) = ∅
400	399	a1i 11	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ℎ ∩ (𝑓 ∖ ℎ)) = ∅)
401		rnss 5599	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑖 ⊆ (𝑔 ↾ ℎ) → ran 𝑖 ⊆ ran (𝑔 ↾ ℎ))
402	382, 401	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → ran 𝑖 ⊆ ran (𝑔 ↾ ℎ))
403		df-ima 5368	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑔 “ ℎ) = ran (𝑔 ↾ ℎ)
404	402, 403	syl6sseqr 3871	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) → ran 𝑖 ⊆ (𝑔 “ ℎ))
405	404	adantr 474	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V) → ran 𝑖 ⊆ (𝑔 “ ℎ))
406	405	ad2antlr 717	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ran 𝑖 ⊆ (𝑔 “ ℎ))
407		incom 4028	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((𝑔 “ ℎ) ∩ ran 𝑗) = (ran 𝑗 ∩ (𝑔 “ ℎ))
408	387, 338	syl6ss 3833	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → 𝑗 ⊆ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))
409		rnss 5599	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ⊢ (𝑗 ⊆ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) → ran 𝑗 ⊆ ran ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))
410	408, 409	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → ran 𝑗 ⊆ ran ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))
411		rnxpss 5820	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 ⊢ ran ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))) ⊆ (𝑏 ∖ (𝑔 “ ℎ))
412	410, 411	syl6ss 3833	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) → ran 𝑗 ⊆ (𝑏 ∖ (𝑔 “ ℎ)))
413	412	ad2antrl 718	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ran 𝑗 ⊆ (𝑏 ∖ (𝑔 “ ℎ)))
414		incom 4028	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑏 ∖ (𝑔 “ ℎ)) ∩ (𝑔 “ ℎ)) = ((𝑔 “ ℎ) ∩ (𝑏 ∖ (𝑔 “ ℎ)))
415		disjdif 4264	. . . . . . . . . . . . . . . . . . . . . . . . . 26 ⊢ ((𝑔 “ ℎ) ∩ (𝑏 ∖ (𝑔 “ ℎ))) = ∅
416	414, 415	eqtri 2802	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((𝑏 ∖ (𝑔 “ ℎ)) ∩ (𝑔 “ ℎ)) = ∅
417		ssdisj 4252	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ ((ran 𝑗 ⊆ (𝑏 ∖ (𝑔 “ ℎ)) ∧ ((𝑏 ∖ (𝑔 “ ℎ)) ∩ (𝑔 “ ℎ)) = ∅) → (ran 𝑗 ∩ (𝑔 “ ℎ)) = ∅)
418	413, 416, 417	sylancl 580	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ran 𝑗 ∩ (𝑔 “ ℎ)) = ∅)
419	407, 418	syl5eq 2826	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ((𝑔 “ ℎ) ∩ ran 𝑗) = ∅)
420		ssdisj 4252	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((ran 𝑖 ⊆ (𝑔 “ ℎ) ∧ ((𝑔 “ ℎ) ∩ ran 𝑗) = ∅) → (ran 𝑖 ∩ ran 𝑗) = ∅)
421	406, 419, 420	syl2anc 579	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ran 𝑖 ∩ ran 𝑗) = ∅)
422		f1oun 6410	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((𝑖:ℎ–1-1-onto→ran 𝑖 ∧ 𝑗:(𝑓 ∖ ℎ)–1-1-onto→ran 𝑗) ∧ ((ℎ ∩ (𝑓 ∖ ℎ)) = ∅ ∧ (ran 𝑖 ∩ ran 𝑗) = ∅)) → (𝑖 ∪ 𝑗):(ℎ ∪ (𝑓 ∖ ℎ))–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
423	396, 398, 400, 421, 422	syl22anc 829	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):(ℎ ∪ (𝑓 ∖ ℎ))–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
424		undif 4273	. . . . . . . . . . . . . . . . . . . . . . . . 25 ⊢ (ℎ ⊆ 𝑓 ↔ (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
425	424	biimpi 208	. . . . . . . . . . . . . . . . . . . . . . . 24 ⊢ (ℎ ⊆ 𝑓 → (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
426	425	adantl 475	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) → (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
427	426	ad2antrr 716	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (ℎ ∪ (𝑓 ∖ ℎ)) = 𝑓)
428	427	f1oeq2d 6387	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ((𝑖 ∪ 𝑗):(ℎ ∪ (𝑓 ∖ ℎ))–1-1-onto→(ran 𝑖 ∪ ran 𝑗) ↔ (𝑖 ∪ 𝑗):𝑓–1-1-onto→(ran 𝑖 ∪ ran 𝑗)))
429	423, 428	mpbid 224	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):𝑓–1-1-onto→(ran 𝑖 ∪ ran 𝑗))
430		f1of1 6390	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((𝑖 ∪ 𝑗):𝑓–1-1-onto→(ran 𝑖 ∪ ran 𝑗) → (𝑖 ∪ 𝑗):𝑓–1-1→(ran 𝑖 ∪ ran 𝑗))
431	429, 430	syl 17	. . . . . . . . . . . . . . . . . . 19 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):𝑓–1-1→(ran 𝑖 ∪ ran 𝑗))
432		ssv 3844	. . . . . . . . . . . . . . . . . . 19 ⊢ (ran 𝑖 ∪ ran 𝑗) ⊆ V
433		f1ss 6356	. . . . . . . . . . . . . . . . . . 19 ⊢ (((𝑖 ∪ 𝑗):𝑓–1-1→(ran 𝑖 ∪ ran 𝑗) ∧ (ran 𝑖 ∪ ran 𝑗) ⊆ V) → (𝑖 ∪ 𝑗):𝑓–1-1→V)
434	431, 432, 433	sylancl 580	. . . . . . . . . . . . . . . . . 18 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → (𝑖 ∪ 𝑗):𝑓–1-1→V)
435		f1eq1 6346	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑒 = (𝑖 ∪ 𝑗) → (𝑒:𝑓–1-1→V ↔ (𝑖 ∪ 𝑗):𝑓–1-1→V))
436	435	rspcev 3511	. . . . . . . . . . . . . . . . . 18 ⊢ (((𝑖 ∪ 𝑗) ∈ 𝒫 𝑔 ∧ (𝑖 ∪ 𝑗):𝑓–1-1→V) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
437	393, 434, 436	syl2anc 579	. . . . . . . . . . . . . . . . 17 ⊢ ((((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) ∧ (𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ)))) ∧ 𝑗:(𝑓 ∖ ℎ)–1-1→V)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
438	437	rexlimdvaa 3214	. . . . . . . . . . . . . . . 16 ⊢ (((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) ∧ (𝑖 ∈ 𝒫 (𝑔 ↾ ℎ) ∧ 𝑖:ℎ–1-1→V)) → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
439	438	rexlimdvaa 3214	. . . . . . . . . . . . . . 15 ⊢ ((𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ℎ ⊆ 𝑓) → (∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
440	255, 223, 439	syl2anc 579	. . . . . . . . . . . . . 14 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → (∃𝑖 ∈ 𝒫 (𝑔 ↾ ℎ)𝑖:ℎ–1-1→V → (∃𝑗 ∈ 𝒫 (𝑔 ∩ ((𝑓 ∖ ℎ) × (𝑏 ∖ (𝑔 “ ℎ))))𝑗:(𝑓 ∖ ℎ)–1-1→V → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
441	275, 381, 440	mp2d 49	. . . . . . . . . . . . 13 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
442	441	ex 403	. . . . . . . . . . . 12 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
443	442	exlimdv 1976	. . . . . . . . . . 11 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → (∃ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ)) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
444	443	imp 397	. . . . . . . . . 10 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ∃ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) ∧ ¬ ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
445	220, 444	sylan2br 588	. . . . . . . . 9 ⊢ (((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) ∧ ¬ ∀ℎ((ℎ ⊊ 𝑓 ∧ ℎ ≠ ∅) → ℎ ≺ (𝑔 “ ℎ))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
446	219, 445	pm2.61dan 803	. . . . . . . 8 ⊢ ((((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) ∧ (𝑔 ∈ 𝒫 (𝑓 × 𝑏) ∧ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑))) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)
447	446	exp32 413	. . . . . . 7 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → (𝑔 ∈ 𝒫 (𝑓 × 𝑏) → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V)))
448	447	ralrimiv 3147	. . . . . 6 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → ∀𝑔 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V))
449		imaeq1 5715	. . . . . . . . . 10 ⊢ (𝑔 = 𝑐 → (𝑔 “ 𝑑) = (𝑐 “ 𝑑))
450	449	breq2d 4898	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → (𝑑 ≼ (𝑔 “ 𝑑) ↔ 𝑑 ≼ (𝑐 “ 𝑑)))
451	450	ralbidv 3168	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) ↔ ∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑)))
452		pweq 4382	. . . . . . . . 9 ⊢ (𝑔 = 𝑐 → 𝒫 𝑔 = 𝒫 𝑐)
453	452	rexeqdv 3341	. . . . . . . 8 ⊢ (𝑔 = 𝑐 → (∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V ↔ ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
454	451, 453	imbi12d 336	. . . . . . 7 ⊢ (𝑔 = 𝑐 → ((∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V) ↔ (∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V)))
455	454	cbvralv 3367	. . . . . 6 ⊢ (∀𝑔 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑔 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑔𝑒:𝑓–1-1→V) ↔ ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
456	448, 455	sylib 210	. . . . 5 ⊢ (((𝑓 ∈ Fin ∧ 𝑏 ∈ Fin) ∧ ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))
457	456	exp31 412	. . . 4 ⊢ (𝑓 ∈ Fin → (𝑏 ∈ Fin → (∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V)) → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
458	457	a2d 29	. . 3 ⊢ (𝑓 ∈ Fin → ((𝑏 ∈ Fin → ∀𝑎(𝑎 ⊊ 𝑓 → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
459	22, 458	syl5bi 234	. 2 ⊢ (𝑓 ∈ Fin → (∀𝑎(𝑎 ⊊ 𝑓 → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑎 × 𝑏)(∀𝑑 ∈ 𝒫 𝑎𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑎–1-1→V))) → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝑓 × 𝑏)(∀𝑑 ∈ 𝒫 𝑓𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝑓–1-1→V))))
460	9, 18, 459	findcard3 8491	1 ⊢ (𝐴 ∈ Fin → (𝑏 ∈ Fin → ∀𝑐 ∈ 𝒫 (𝐴 × 𝑏)(∀𝑑 ∈ 𝒫 𝐴𝑑 ≼ (𝑐 “ 𝑑) → ∃𝑒 ∈ 𝒫 𝑐𝑒:𝐴–1-1→V)))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 198   ∧ wa 386  ∀wal 1599   = wceq 1601  ∃wex 1823   ∈ wcel 2107   ≠ wne 2969  ∀wral 3090  ∃wrex 3091  Vcvv 3398   ∖ cdif 3789   ∪ cun 3790   ∩ cin 3791   ⊆ wss 3792   ⊊ wpss 3793  ∅c0 4141  𝒫 cpw 4379  {csn 4398  ⟨cop 4404   class class class wbr 4886   × cxp 5353  ran crn 5356   ↾ cres 5357   “ cima 5358  –1-1→wf1 6132  –1-1-onto→wf1o 6134   ≈ cen 8238   ≼ cdom 8239   ≺ csdm 8240  Fincfn 8241

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-ral 3095  df-rex 3096  df-rab 3099  df-v 3400  df-sbc 3653  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-br 4887  df-opab 4949  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-om 7344  df-1o 7843  df-er 8026  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245

This theorem is referenced by:  marypha1  8628