fin1a2lem12 - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > fin1a2lem12		Structured version Visualization version GIF version

Theorem fin1a2lem12 10396

Description: Lemma for fin1a2 10400. (Contributed by Stefan O'Rear, 8-Nov-2014.) (Revised by Mario Carneiro, 17-May-2015.)

**Assertion**
Ref	Expression
fin1a2lem12	⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ¬ 𝐵 ∈ Fin^III)

Proof of Theorem fin1a2lem12 Dummy variables 𝑑 𝑒 𝑓 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		simpr 489	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐵 ∈ Fin^III)
2		simpll1 1231	. . . . . . 7 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐴 ⊆ 𝒫 𝐵)
3	2	adantr 485	. . . . . 6 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → 𝐴 ⊆ 𝒫 𝐵)
4		ssrab2 4035	. . . . . . . 8 ⊢ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐴
5	4	unissi 4882	. . . . . . 7 ⊢ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ ∪ 𝐴
6		sspwuni 5067	. . . . . . . 8 ⊢ (𝐴 ⊆ 𝒫 𝐵 ↔ ∪ 𝐴 ⊆ 𝐵)
7	6	biimpi 219	. . . . . . 7 ⊢ (𝐴 ⊆ 𝒫 𝐵 → ∪ 𝐴 ⊆ 𝐵)
8	5, 7	sstrid 3949	. . . . . 6 ⊢ (𝐴 ⊆ 𝒫 𝐵 → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵)
9	3, 8	syl 18	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵)
10		elpw2g 5305	. . . . . 6 ⊢ (𝐵 ∈ Fin^III → (∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ∈ 𝒫 𝐵 ↔ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵))
11	10	ad2antlr 739	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → (∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ∈ 𝒫 𝐵 ↔ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ⊆ 𝐵))
12	9, 11	mpbird 260	. . . 4 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑒 ∈ ω) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} ∈ 𝒫 𝐵)
13	12	fmpttd 7112	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}):ω⟶𝒫 𝐵)
14		vex 3459	. . . . . . . . . . 11 ⊢ 𝑑 ∈ V
15	14	sucex 7806	. . . . . . . . . 10 ⊢ suc 𝑑 ∈ V
16		sssucid 6445	. . . . . . . . . 10 ⊢ 𝑑 ⊆ suc 𝑑
17		ssdomg 8998	. . . . . . . . . 10 ⊢ (suc 𝑑 ∈ V → (𝑑 ⊆ suc 𝑑 → 𝑑 ≼ suc 𝑑))
18	15, 16, 17	mp2 9	. . . . . . . . 9 ⊢ 𝑑 ≼ suc 𝑑
19		domtr 9005	. . . . . . . . 9 ⊢ ((𝑓 ≼ 𝑑 ∧ 𝑑 ≼ suc 𝑑) → 𝑓 ≼ suc 𝑑)
20	18, 19	mpan2 703	. . . . . . . 8 ⊢ (𝑓 ≼ 𝑑 → 𝑓 ≼ suc 𝑑)
21	20	a1i 11	. . . . . . 7 ⊢ (𝑓 ∈ 𝐴 → (𝑓 ≼ 𝑑 → 𝑓 ≼ suc 𝑑))
22	21	ss2rabi 4031	. . . . . 6 ⊢ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑}
23		uniss 4881	. . . . . 6 ⊢ ({𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
24	22, 23	mp1i 14	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ⊆ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
25		id 23	. . . . . 6 ⊢ (𝑑 ∈ ω → 𝑑 ∈ ω)
26		pwexg 5351	. . . . . . . . 9 ⊢ (𝐵 ∈ Fin^III → 𝒫 𝐵 ∈ V)
27	26	adantl 486	. . . . . . . 8 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝒫 𝐵 ∈ V)
28	27, 2	ssexd 5296	. . . . . . 7 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐴 ∈ V)
29		rabexg 5309	. . . . . . 7 ⊢ (𝐴 ∈ V → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V)
30		uniexg 7740	. . . . . . 7 ⊢ ({𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V)
31	28, 29, 30	3syl 19	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V)
32		breq2 5114	. . . . . . . . 9 ⊢ (𝑒 = 𝑑 → (𝑓 ≼ 𝑒 ↔ 𝑓 ≼ 𝑑))
33	32	rabbidv 3423	. . . . . . . 8 ⊢ (𝑒 = 𝑑 → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
34	33	unieqd 4886	. . . . . . 7 ⊢ (𝑒 = 𝑑 → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
35		eqid 2763	. . . . . . 7 ⊢ (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})
36	34, 35	fvmptg 6989	. . . . . 6 ⊢ ((𝑑 ∈ ω ∧ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑} ∈ V) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
37	25, 31, 36	syl2anr 608	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑑})
38		peano2 7887	. . . . . 6 ⊢ (𝑑 ∈ ω → suc 𝑑 ∈ ω)
39		rabexg 5309	. . . . . . 7 ⊢ (𝐴 ∈ V → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V)
40		uniexg 7740	. . . . . . 7 ⊢ ({𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V)
41	28, 39, 40	3syl 19	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V)
42		breq2 5114	. . . . . . . . 9 ⊢ (𝑒 = suc 𝑑 → (𝑓 ≼ 𝑒 ↔ 𝑓 ≼ suc 𝑑))
43	42	rabbidv 3423	. . . . . . . 8 ⊢ (𝑒 = suc 𝑑 → {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
44	43	unieqd 4886	. . . . . . 7 ⊢ (𝑒 = suc 𝑑 → ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒} = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
45	44, 35	fvmptg 6989	. . . . . 6 ⊢ ((suc 𝑑 ∈ ω ∧ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑} ∈ V) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
46	38, 41, 45	syl2anr 608	. . . . 5 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑) = ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ suc 𝑑})
47	24, 37, 46	3sstr4d 3993	. . . 4 ⊢ (((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) ∧ 𝑑 ∈ ω) → ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑))
48	47	ralrimiva 3157	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∀𝑑 ∈ ω ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑))
49		fin34i 10366	. . 3 ⊢ ((𝐵 ∈ Fin^III ∧ (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}):ω⟶𝒫 𝐵 ∧ ∀𝑑 ∈ ω ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘𝑑) ⊆ ((𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})‘suc 𝑑)) → ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}))
50	1, 13, 48, 49	syl3anc 1398	. 2 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}))
51		fin1a2lem11 10395	. . . . . 6 ⊢ (( [⊊] Or 𝐴 ∧ 𝐴 ⊆ Fin) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
52	51	adantrr 729	. . . . 5 ⊢ (( [⊊] Or 𝐴 ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
53	52	3ad2antl2 1205	. . . 4 ⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
54	53	adantr 485	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
55		simpll3 1233	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ 𝐴 ∈ 𝐴)
56		simplrr 789	. . . . . . 7 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → 𝐴 ≠ ∅)
57		sspwuni 5067	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ ∪ 𝐴 ⊆ ∅)
58		ss0b 4359	. . . . . . . . . . 11 ⊢ (∪ 𝐴 ⊆ ∅ ↔ ∪ 𝐴 = ∅)
59	57, 58	bitri 278	. . . . . . . . . 10 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ ∪ 𝐴 = ∅)
60		pw0 4779	. . . . . . . . . . . . 13 ⊢ 𝒫 ∅ = {∅}
61	60	sseq2i 3967	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ 𝐴 ⊆ {∅})
62		sssn 4793	. . . . . . . . . . . 12 ⊢ (𝐴 ⊆ {∅} ↔ (𝐴 = ∅ ∨ 𝐴 = {∅}))
63	61, 62	bitri 278	. . . . . . . . . . 11 ⊢ (𝐴 ⊆ 𝒫 ∅ ↔ (𝐴 = ∅ ∨ 𝐴 = {∅}))
64		df-ne 2959	. . . . . . . . . . . 12 ⊢ (𝐴 ≠ ∅ ↔ ¬ 𝐴 = ∅)
65		0ex 5271	. . . . . . . . . . . . . . . . 17 ⊢ ∅ ∈ V
66	65	unisn 4892	. . . . . . . . . . . . . . . 16 ⊢ ∪ {∅} = ∅
67	65	snid 4629	. . . . . . . . . . . . . . . 16 ⊢ ∅ ∈ {∅}
68	66, 67	eqeltri 2859	. . . . . . . . . . . . . . 15 ⊢ ∪ {∅} ∈ {∅}
69		unieq 4884	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 = {∅} → ∪ 𝐴 = ∪ {∅})
70		id 23	. . . . . . . . . . . . . . . 16 ⊢ (𝐴 = {∅} → 𝐴 = {∅})
71	69, 70	eleq12d 2857	. . . . . . . . . . . . . . 15 ⊢ (𝐴 = {∅} → (∪ 𝐴 ∈ 𝐴 ↔ ∪ {∅} ∈ {∅}))
72	68, 71	mpbiri 261	. . . . . . . . . . . . . 14 ⊢ (𝐴 = {∅} → ∪ 𝐴 ∈ 𝐴)
73	72	orim2i 923	. . . . . . . . . . . . 13 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (𝐴 = ∅ ∨ ∪ 𝐴 ∈ 𝐴))
74	73	ord 877	. . . . . . . . . . . 12 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (¬ 𝐴 = ∅ → ∪ 𝐴 ∈ 𝐴))
75	64, 74	biimtrid 245	. . . . . . . . . . 11 ⊢ ((𝐴 = ∅ ∨ 𝐴 = {∅}) → (𝐴 ≠ ∅ → ∪ 𝐴 ∈ 𝐴))
76	63, 75	sylbi 220	. . . . . . . . . 10 ⊢ (𝐴 ⊆ 𝒫 ∅ → (𝐴 ≠ ∅ → ∪ 𝐴 ∈ 𝐴))
77	59, 76	sylbir 238	. . . . . . . . 9 ⊢ (∪ 𝐴 = ∅ → (𝐴 ≠ ∅ → ∪ 𝐴 ∈ 𝐴))
78	77	com12 33	. . . . . . . 8 ⊢ (𝐴 ≠ ∅ → (∪ 𝐴 = ∅ → ∪ 𝐴 ∈ 𝐴))
79	78	con3d 153	. . . . . . 7 ⊢ (𝐴 ≠ ∅ → (¬ ∪ 𝐴 ∈ 𝐴 → ¬ ∪ 𝐴 = ∅))
80	56, 55, 79	sylc 66	. . . . . 6 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ 𝐴 = ∅)
81		ioran 999	. . . . . 6 ⊢ (¬ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅) ↔ (¬ ∪ 𝐴 ∈ 𝐴 ∧ ¬ ∪ 𝐴 = ∅))
82	55, 80, 81	sylanbrc 594	. . . . 5 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅))
83		uniun 4896	. . . . . . . 8 ⊢ ∪ (𝐴 ∪ {∅}) = (∪ 𝐴 ∪ ∪ {∅})
84	66	uneq2i 4120	. . . . . . . 8 ⊢ (∪ 𝐴 ∪ ∪ {∅}) = (∪ 𝐴 ∪ ∅)
85		un0 4352	. . . . . . . 8 ⊢ (∪ 𝐴 ∪ ∅) = ∪ 𝐴
86	83, 84, 85	3eqtri 2790	. . . . . . 7 ⊢ ∪ (𝐴 ∪ {∅}) = ∪ 𝐴
87	86	eleq1i 2854	. . . . . 6 ⊢ (∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}) ↔ ∪ 𝐴 ∈ (𝐴 ∪ {∅}))
88		elun 4108	. . . . . 6 ⊢ (∪ 𝐴 ∈ (𝐴 ∪ {∅}) ↔ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 ∈ {∅}))
89	65	elsn2 4632	. . . . . . 7 ⊢ (∪ 𝐴 ∈ {∅} ↔ ∪ 𝐴 = ∅)
90	89	orbi2i 925	. . . . . 6 ⊢ ((∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 ∈ {∅}) ↔ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅))
91	87, 88, 90	3bitri 300	. . . . 5 ⊢ (∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}) ↔ (∪ 𝐴 ∈ 𝐴 ∨ ∪ 𝐴 = ∅))
92	82, 91	sylnibr 332	. . . 4 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅}))
93		unieq 4884	. . . . . 6 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = ∪ (𝐴 ∪ {∅}))
94		id 23	. . . . . 6 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}))
95	93, 94	eleq12d 2857	. . . . 5 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → (∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ↔ ∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅})))
96	95	notbid 321	. . . 4 ⊢ (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → (¬ ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ↔ ¬ ∪ (𝐴 ∪ {∅}) ∈ (𝐴 ∪ {∅})))
97	92, 96	syl5ibrcom 250	. . 3 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → (ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) = (𝐴 ∪ {∅}) → ¬ ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒})))
98	54, 97	mpd 16	. 2 ⊢ ((((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) ∧ 𝐵 ∈ Fin^III) → ¬ ∪ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}) ∈ ran (𝑒 ∈ ω ↦ ∪ {𝑓 ∈ 𝐴 ∣ 𝑓 ≼ 𝑒}))
99	50, 98	pm2.65da 828	1 ⊢ (((𝐴 ⊆ 𝒫 𝐵 ∧ [⊊] Or 𝐴 ∧ ¬ ∪ 𝐴 ∈ 𝐴) ∧ (𝐴 ⊆ Fin ∧ 𝐴 ≠ ∅)) → ¬ 𝐵 ∈ Fin^III)

Colors of variables: wff setvar class

Syntax hints: ¬ wn 3 → wi 4 ↔ wb 209 ∧ wa 400 ∨ wo 860 ∧ w3a 1103 = wceq 1570 ∈ wcel 2143 ≠ wne 2958 ∀wral 3079 {crab 3416 Vcvv 3455 ∪ cun 3904 ⊆ wss 3906 ∅c0 4287 𝒫 cpw 4563 {csn 4590 ∪ cuni 4873 class class class wbr 5110 ↦ cmpt 5193 Or wor 5570 ran crn 5664 suc csuc 6364 ⟶wf 6534 ‘cfv 6538 [⊊] crpss 7721 ωcom 7863 ≼ cdom 8942 Fincfn 8944 Fin^IIIcfin3 10266

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5239 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3080 df-rex 3090 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-int 4914 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-tr 5220 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 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-isom 6547 df-riota 7369 df-ov 7415 df-rpss 7722 df-om 7864 df-2nd 7988 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-1o 8454 df-er 8695 df-en 8945 df-dom 8946 df-sdom 8947 df-fin 8948 df-wdom 9528 df-card 9926 df-fin4 10272 df-fin3 10273

This theorem is referenced by: fin1a2s 10399

W3C validator